Navier–Stokes Millennium Prize problem: finite-time breakdown with smooth forcing
For the three-dimensional incompressible Navier–Stokes equations with positive viscosity, do there exist smooth divergence-free initial data and smooth external forcing for which a global smooth physically reasonable solution does not exist? The Clay Millennium Prize formulation allows this to be established either on R^3 (statement C) or on the periodic three-torus (statement D).
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- PDEs; fluid dynamics; singularity formation
- Posed by
- Charles L. Fefferman, Clay Mathematics Institute
- Year posed
- 2000
- Years open
- 26y
- Solved
- 2026-09-05
- Model
- Unnamed internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- 87 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
OpenAI claims to construct a smooth finite-energy solution of the three-dimensional incompressible Navier–Stokes equations, starting from a fluid at rest and driven by smooth forcing, that develops a finite-time singularity. The construction is claimed both on R^3 and in the periodic setting, thereby establishing statements C and D of Fefferman's official Clay formulation. If the correspondence between the released proof/formalization and the Clay statements survives independent review, this resolves the Navier–Stokes Millennium Prize problem. It does not establish finite-time blow-up for the unforced Navier–Stokes equations; the Clay resolution comes through the smooth-forcing alternatives C/D.
What the AI did
OpenAI launched a multi-agent research effort using an unnamed internal model significantly more capable than GPT-6 Astra. Roughly 10,000 concurrent agents explored the Navier–Stokes Millennium Prize problem, with separate groups assigned the different Clay formulations and related subproblems. After the system independently found an unforced 3D Euler blow-up construction, that result was supplied to the Navier–Stokes agents. Codex was used to consolidate useful intermediate insights across groups. The system produced the analytical finite-time singularity construction after approximately 88 hours. GPT-6 Astra was subsequently used to formalize and verify the result in Lean.
Verification
Audited here on 9 September 2026. Statement anchor: OpenAI's ComparatorChallenges/NavierStokes.lean was diffed against google-deepmind/formal-conjectures at commit 8bf45ed, the commit its header names. The two compared theorems, navier_stokes_breakdown_R3 and navier_stokes_breakdown_periodic, are byte-identical to DeepMind's, as are the decay, periodicity and energy conditions they depend on; the only differences in the file are nine deleted lines carrying Formal Conjectures' alternatives (A) and (B), which OpenAI does not claim. The statement is therefore anchored to an independent third party's formalisation of Fefferman's conditions, not to one written by the prover. Counts taken independently: 2,486 Lean files, 616,276 lines, zero sorry outside the deliberate challenge placeholders, zero axiom declarations, zero native_decide, zero unsafe. comparator.json permits only propext, Quot.sound and Classical.choice and enables the independent nanoda kernel; the solution module states both theorems verbatim and discharges them via ComparatorBridge. In the paper, Theorem 1.1's force lies in C^inf_c(R^3 x (0,inf)), compactly supported in space and time, satisfying Fefferman's decay condition (5) outright. Not rebuilt here. No mathematician has read the argument: released 8 September 2026, no referee, and Clay's own process requires publication in a refereed journal plus two years of general acceptance.
Sources
- Lean proofThe Lean development and comparator configuration
- Lean statementOpenAI's comparator challenge statement for (C) and (D)
- AnnouncementOpenAI research publication and proof announcement
- Problem recordFormal Conjectures' original, which the statement matches byte for byteFefferman's official Clay problem description
- OtherClay Mathematics Institute — official Navier–Stokes formulation
Submitted by LucidHawk551 on
Should the unforced Euler equation blowup be moved into a separate result? It is an important result in its own right.