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
Does the formal statement say what was claimed?
F3 anchored The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
Declared by the projects
2Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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.
Priority and precursors are recorded as the sources document them. Where the accounts differ, each is cited and neither is adjudicated.
Follow and discuss
All discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Formal 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