Claimed AI-led

Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D

A Lean development proves that three-dimensional Navier-Stokes with a smooth forcing term breaks down in finite time, at every positive viscosity, on both Euclidean space and the periodic torus, which is two of the four statements the Clay problem description asks for a proof of, though not the unforced regularity question the phrase usually brings to mind.

Lab: OpenAI
Model: Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization
Field: Mathematics
Date: 2026-09-08
Problem posed: 2000 · open 26 yrs

Sources

What was found

Fefferman's Clay problem description asks for a proof of one of four statements, offered as leeway to solvers while, in his words, retaining the heart of the problem. This work settles (C) and (D), the two breakdown alternatives, both of which permit a smooth external force meeting the decay conditions the description imposes: for every positive viscosity there exist smooth initial data and forcing admitting no global smooth solution of uniformly bounded kinetic energy on $\mathbb{R}^3$ , and smooth periodic data and forcing admitting no global smooth solution on $\mathbb{R}^3/\mathbb{Z}^3$ . The repository carries Lean 4 proofs of both, declared as navier_stokes_breakdown_R3 and navier_stokes_breakdown_periodic, each recorded with no sorry and depending on exactly propext, Classical.choice and Quot.sound. The Comparator reference statements were adapted from Google DeepMind's Formal Conjectures formalization of the Clay problem rather than written for this repository, and the challenge config enables the independent nanoda kernel. The same repository also carries two theorems on unforced Euler blowup, which are a separate result and are not covered by this entry.

Novelty check

The alternatives settled here are Clay's own (C) and (D), stated in Fefferman's 2000 problem description, which the repository cites and links directly; the underlying regularity question goes back to Leray in 1934. The prior literature on forced or modified blowup is substantial but does not reach full three-dimensional Navier-Stokes with smooth forcing: blowup is known for the hypodissipative equations with a force (arXiv:2407.06776), for solutions with linear growth at infinity (arXiv:2103.12237), and for model equations (arXiv:1811.09394), and Tao's averaged Navier-Stokes construction is of the same character. No prior claim on (C) or (D) themselves was found in the four registries or in that search. The live novelty question is not priority over the classical literature but priority within the past year: OpenAI's own account credits the basic idea of the program to Diego Cordoba and Luis Martinez-Zoroa, and how much is owed to that program is publicly disputed, which the caveats record.

Caveats and known objections

What this settles, and what it does not, needs stating carefully. Fefferman's problem description asks for a proof of any one of four statements, and the breakdown alternatives (C) and (D) are two of them, so on the problem as officially posed this is a candidate solution to the Millennium Prize Problem rather than something adjacent to it. The Clay Mathematics Institute said as much on 2026-09-11, that the problem has 'apparently been settled', while noting that its own process for evaluating the work and assigning credit is deliberately unhurried. What the result is not is a resolution of the unforced regularity question, alternatives (A) and (B), which is what the phrase 'the Navier-Stokes problem' is usually taken to name and what a reader of the press coverage would most likely assume was meant. The repository's README names the alternatives precisely and links Clay's own description, which is more care than most of that coverage took. Verification is graded claimed rather than formal despite four theorems carrying no sorry and exactly the three standard axioms, for the reason the repository itself supplies: its formalization.yaml records the review status as self-assessed, and no mathematician outside OpenAI is on record as having read the argument. Clay's own acceptance process additionally requires journal publication and two years of community acceptance. The statement-fidelity worry is smaller here than on a self-stated formalization, because the Comparator challenge statements were adapted from DeepMind's independent Formal Conjectures formalization rather than authored alongside the proof, and vibemathed has since diffed the adaptation: the two compared theorems and the conditions they depend on are byte-identical to DeepMind's file, the only difference being nine deleted lines carrying alternatives (A) and (B), which OpenAI does not claim. The model attribution is split, and both halves are recorded above because they may describe different steps: the announcement describes an unnamed next-generation model more capable than GPT-6 Astra, reported as roughly 10,000 coordinating agents over 88 hours, while the repository's own metadata credits GPT-6 Astra through Codex under an agent method, which most plausibly describes who wrote the Lean rather than who found the proof. Autonomy is ai-led rather than autonomous because the disclosure describes an agent framework without stating that the run was unsteered, so the strictest defensible reading is not autonomous. Priority is contested in public and unresolved at entry: the entangled Alpoge and Buckmaster results released the same week drew allegations, on r/math and in the comments of Terence Tao's blog, that the Cordoba and Martinez-Zoroa program was worked from for roughly a year before a denial that several commenters read as evasive, and Andreas Thom has publicly described asking OpenAI whether his own private conversations on an adjacent problem were drawn on and being told they were not, without further explanation. None of that bears on whether the Lean compiles.

Independent checks

vibemathed.com statement audit: Diffed ComparatorChallenges/NavierStokes.lean against google-deepmind/formal-conjectures at 8bf45ed: both compared theorems and their decay, periodicity and energy conditions are byte-identical, with alternatives (A) and (B) removed. Counted no sorry outside the placeholders and no axiom declarations. Not rebuilt; no mathematician has read the argument. · link ↗

Also recorded at

vibemathednavier-stokes-millennium-prize-problem-finite-time-breakdown-with-smooth-forcing

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

Recorded there as a candidate with review pending.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

History of this entry

2026-09-24CheckedRecorded vibemathed's diff showing the compared statements are DeepMind's Formal Conjectures formalization verbatim. Nobody outside OpenAI has read the argument, so no grade moved. source ↗
2026-09-22ChallengedCited the first independent technical engagement with the construction: Constantin, Ignatova and Vicol prove that a solution with the announced anisotropic Type II bounds and a collapsing axisymmetric core is regular at the putative singular point under a real-analytic force, so the force can neither vanish near that point nor be real-analytic in space. It constrains the construction rather than refuting it, and no grade moved. source ↗
2026-09-14CorrectedCorrected what the Clay prize covers. This entry originally said the Millennium Prize attaches only to alternatives (A) and (B) and that the result therefore was not the Millennium problem. Fefferman's problem description asks for a proof of any one of four statements, and the breakdown alternatives (C) and (D) are two of them, so the result is a candidate solution to the problem as posed. Added the Clay Mathematics Institute's statement of 2026-09-11. Neither grade moved. source ↗
2026-09-10AddedEntered the registry graded Claimed and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Community discussion

Hacker NewsOn the Navier-Stokes Millennium Prize Problem↗Hacker NewsHow an AI math breakthrough ignited a controversy↗

Graded claimed for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-08-navier-stokes-forced-blowup

BibTeX

@misc{whataifound-openai-2026-blowup,
  title        = {Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by OpenAI. Verification: Claimed. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-09-08-navier-stokes-forced-blowup}
}

Related findings

ClaimedFinite-time blowup for the unforced Euler equations from smooth compactly supported dataOpenAI · 2026-09-08 ClaimedFinite-time blowup for the IPM equation with uniformly space-time smooth forcingIndependent · 2026-09-15 Claimed722 manuscripts in 372 result families from an unreleased OpenAI modelOpenAI · 2026-10-06

pde fluid-dynamics navier-stokes singularity lean formalization argument

← All mathematics findings in the registry

Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D

Sources

Original work

Announcement

Media coverage

Independent commentary

Challenge