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, settling two of the four alternatives the Clay problem description lists but not the unforced question the Millennium Prize attaches to.
- 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
Original work
Announcement
Media coverage
Independent commentary
Challenge
What was found
Fefferman's Clay problem description lists four alternatives, and the Millennium Prize attaches to (A) and (B), global existence and smoothness for the unforced equations. This work settles (C) and (D), the two breakdown alternatives, which permit a forcing term: for every positive viscosity there exist smooth initial data and forcing admitting no global smooth solution of uniformly bounded kinetic energy on R^3, and smooth periodic data and forcing admitting no global smooth solution on R^3/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
This is not the Millennium Prize problem and the entry should not be read as saying it is. The prize attaches to the unforced equations, alternatives (A) and (B); (C) and (D) permit a forcing term. The repository's README is explicit about that distinction, while OpenAI's blog post is titled 'On the Navier-Stokes Millennium Prize Problem' and much of the press coverage dropped it entirely. 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, but that adaptation has not itself been checked by a third party. 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.
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.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered 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.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
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-blowupBibTeX
@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}
}