Millennium·millennium:NavierStokes
Existence and Smoothness of the Navier–Stokes Equation
No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.
Fidelity F3: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.
AI activity
How grades workFinite-time blowup for the 3D incompressible Navier–Stokes equations with smooth forcing, on Euclidean space and on the torus: Fefferman's alternatives (C) and (D), a negative answer to the Millennium problem. Unforced Euler blowup is proved alongside.
Reasoning and sources
Autonomy
By OpenAI's account some 10,000 agents worked for 88 hours with little human mathematical input. The run was aimed at a problem the Córdoba–Martínez-Zoroa programme had already brought within reach, and began after reports of the Buckmaster–Alpöge work reached OpenAI. A2 records a result the system produced on framing it was given.
Details
compute: At least 10,000 agents over an 88-hour run from 1 September; 2.7 million messages and 130 billion output tokens in the run that produced the proof
paper: 166 pages, revised to cite Córdoba and Martínez-Zoroa
Formalised the Navier–Stokes and Euler results in Lean, checked with Comparator against the Formal Conjectures statements of alternatives (C) and (D).
Reasoning and sources
Autonomy
Formalisation of a proof found by another system; the project's formalization.yaml records the method as an agent in Codex.
Details
scale: 2,659 Lean files, about 33 MB of source
Fidelity
How fidelity is gradedF3 anchored. The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.
Declared by the projects
2As each project's formalization.yaml states it.
Navier–Stokes critical-norm reduction on R3 (checkpoint CP1)
- authors
- Christopher Albert
- method
- agent — claude-fable-5-1, claude-opus-5, claude-sonnet-5
- review
- self-assessed — self-assessed; within-family independent audits recorded in itpplasma/navier (none)
- sorry
- 9 unproved goals declared
- sources
- Internal CP1 proof development for the Navier–Stokes critical-norm route — other; Existence and smoothness of the Navier–Stokes equation — background; Localisation and compactness properties of the Navier–Stokes global regularity problem — background; A profile decomposition approach to the L∞_t(L³_x) Navier–Stokes regularity criterion — background
- related
- google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millenium/NavierStokes.lean — builds-on; openai/NavierStokesAndEuler — builds-on
- divergences
- none known; statement audit pending
- checked by
- nobody independent of its authors yet
NavierStokesAndEuler
- authors
- OpenAI
- method
- agent — GPT-6 Astra
- review
- self-assessed
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 0 unproved goals declared
- results
- 4 main results named, checked with Comparator, with an alignment table
- sources
- Finite time blowup for Navier–Stokes — formalizes; Finite time blowup for the Euler equation — formalizes
- related
- google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millenium/NavierStokes.lean — builds-on
- checked by
- nobody independent of its authors yet
Provenance
Built on
- Thomas Hou and Guo Luo 2013
Numerical evidence that solutions of the 3D Euler equations can blow up in finite time. Source
- Diego Córdoba and Luis Martínez-Zoroa 2023
An analytic programme for constructing finite-time blowup, which with Fan Zheng gave unforced blowup for 3D Euler and forced blowup for hypodissipative Navier–Stokes. Both teams that reached the Millennium setting built on it. Source
Concurrent work
- Tristan Buckmaster and Levent Alpöge 2026-08-22, announced 2026-09-07
Blowup with smooth forcing for Euler, the incompressible porous media equation and Boussinesq, obtained on 15 August with AI assistance and verified in Lean a week later. Announced about twelve hours before OpenAI. Source
In dispute
- Priority and customer data
Buckmaster says news of the pair's progress reached OpenAI before its run, and asks whether their use of Codex informed the model. OpenAI's account changed between 8 and 13 September, ending with the statement that no user input after 3 July could have influenced the system. Source
- Attribution
The first version of OpenAI's paper did not cite Córdoba and Martínez-Zoroa. The references were added in the 166-page revision. Source
Prize
Clay Millennium Prize: OpenAI does not intend to claim it, and the Clay Mathematics Institute has acknowledged no party.
Follow and discuss
All discussionFollow this problem
An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.
Discussion and bounties for this problem load here.
Seen recently
What the monitors picked up in the last thirty days, not yet graded.
Something wrong or missing here? Request a correction or add a claim, with its sources.
Claims and corrections from readers
All of themFormal material
Formal statements · 1
Recorded elsewhere
Compare the registries- vibemathed — Navier–Stokes Millennium Prize problem: finite-time breakdown with smooth forcing
- vibemathed — Finite-time blowup for the 3D incompressible Euler equations from smooth data
Also known as · 2
- https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millennium/NavierStokes.lean
- FormalConjectures/Millennium/NavierStokes.lean
Cite this record
qed.bot, “Existence and Smoothness of the Navier–Stokes Equation”, https://qed.bot/s/millennium-navierstokes, as of 30 Sep 2026.