# Existence and Smoothness of the Navier–Stokes Equation

A statement in qed.bot, the register of claims of AI work in mathematics. The register grades the evidence attached to each claim; it never rules on whether a proof is correct.

- Identifier: millennium:NavierStokes
- Collection: Millennium
- Page: https://qed.bot/s/millennium-navierstokes
- Formal record: mixed
- Machine-checked: no independent check has verified it
- Fidelity F3: The project checks its proof with Comparator against a statement from a corpus written separately from the proof, and held here.
- Source: https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millennium/NavierStokes.lean

## AI claims

### OpenAI internal model, 8 Sep 2026

Finite-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.

- Outcome: full
- Autonomy A2: Directed. The system produced the result while building on literature or framing supplied to it.
- Evidence V2: Artifact reported. A proof or a constructed object is published, but nobody independent of its authors has rebuilt it.
- Fidelity F3: Anchored. The proof is checked for exact statement identity against a statement written independently of it, held here from a separate statement corpus.
- Source: OpenAI, On the Navier–Stokes Millennium Prize Problem, https://openai.com/index/navier-stokes-solution/
- Source: Lean formalisation, https://github.com/openai/NavierStokesAndEuler
- Source: Quanta, AI has solved one of math's $1 million Millennium Prize Problems, https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/
- Source: Wikipedia, Navier–Stokes priority controversy, https://en.wikipedia.org/wiki/Navier%E2%80%93Stokes_priority_controversy

### GPT-6 Astra, 9 Sep 2026

Formalised the Navier–Stokes and Euler results in Lean, checked with Comparator against the Formal Conjectures statements of alternatives (C) and (D).

- Outcome: full (a supporting task)
- Autonomy A1: Collaborative. A human and a system worked the problem together, or the system played a supporting role.
- Evidence V2: Artifact reported. A proof or a constructed object is published, but nobody independent of its authors has rebuilt it.
- Fidelity F3: Anchored. The proof is checked for exact statement identity against a statement written independently of it, held here from a separate statement corpus.
- Source: Lean formalisation, https://github.com/openai/NavierStokesAndEuler
- Source: formalization.yaml, https://github.com/openai/NavierStokesAndEuler/blob/main/formalization.yaml

## Formal statements

- FormalConjectures/Millennium/NavierStokes.lean, https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Millennium/NavierStokes.lean

Cite as: qed.bot, "Existence and Smoothness of the Navier–Stokes Equation", https://qed.bot/s/millennium-navierstokes, as of 30 Sep 2026. The register's data is published under CC BY 4.0: https://creativecommons.org/licenses/by/4.0/