AI-generated Navier-Stokes finite-time blow-up proof (with Lean formalization)
OpenAI claims an internal agent system proved a Navier-Stokes finite-time singularity with smooth forcing, resolving the Millennium Prize problem, with a Lean proof.
About 10,000 concurrent agents took roughly 88 hours; 17 more hours of Lean formalization; 4.9 million messages and about 300 billion output tokens across all problems tried. Builds on Cordoba and Martinez-Zoroa's method. The result is disputed. A rival NYU/Anthropic Euler result appeared hours earlier, and a Fields-medalist declaration reportedly criticized the practice.
- Date
- Tuesday, 8 September 2026
- Lab
- OpenAI
- Kind
- paper
- Access
- research preview
Figures
| Measure | Value | Measured by |
|---|---|---|
| Agents on the Navier-Stokes group | about 10,000 concurrent; 88 hours plus 17 hours Lean 2.7M messages and about 130B output tokens for this problem | company |
| Output tokens across all attempted problems | about 300 billion 4.9 million agent messages | mixed |
No Clay Institute award was reported in the sources read. Quanta says the result extends a method of Cordoba and Martinez-Zoroa and passed Lean checking, but humans must confirm the Lean statement matches the intended problem. A 2026-09-11 declaration reportedly signed by 28 Fields medalists criticized the practice (single search summary, not read).
Sources
- openai.com/index/navier-stokes-solution/
- simonwillison.net/2026/Sep/8/on-navier-stokes/
- www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-2026
This record was checked against its sources on 6 October 2026. How we check