OpenAI has announced a proposed solution to the Navier-Stokes existence and smoothness problem, one of the seven Millennium Prize Problems.
As a mechanical engineer, that is a strange sentence to read. These equations are fundamental to how we understand fluid motion. Now an AI lab says its system has resolved a question about them that has remained open for roughly 90 years.
The announcement was published on September 8. OpenAI released a mathematical writeup and a formalization in Lean, although the claim still needs independent scrutiny. Read the announcement
What does “solving Navier-Stokes” mean?
The equations describe how fluids move. Engineers already use them to study airflow, water flow, and other physical systems.
The Millennium Problem asks a more fundamental question: under the specified conditions, do smooth three-dimensional fluid flows remain smooth, or can they break down?
OpenAI claims an initially smooth fluid at rest can develop a singularity under a smooth external force. In its construction, velocity grows without bound in finite time, while the fluid’s energy remains finite. The claim concerns the mathematical model, not real water suddenly moving infinitely fast. OpenAI’s description of the result
The external force does not automatically disqualify the result. Clay’s official formulation explicitly includes breakdown cases with smooth forcing. OpenAI says its proof establishes alternatives C and D. Clay’s official problem statement
How the agents approached it
OpenAI used an unreleased internal model that it describes as significantly more capable than GPT-6 Astra.
The effort initially covered several mathematical problems. After agents produced an earlier result on the unforced Euler equations, researchers concentrated resources on Navier-Stokes and shared intermediate findings between groups.
Euler equations remove viscosity. “Unforced” means no external force is applied. Those are separate distinctions.
| Part of the effort | OpenAI’s reported figure |
|---|---|
| Concurrent agents in the successful group | Roughly 10,000 |
| Time from the first agents launching to resolution | About 88 hours |
| Additional Lean formalization and verification using GPT-6 Astra | 17 hours |
| Output tokens used for the Navier-Stokes effort | Approximately 130 billion |
These figures describe a coordinated research effort with human steering and substantial compute. How OpenAI says it found the proof
What the Lean verification establishes
Lean is a programming language and theorem prover. Its checking system can verify that a formal proof follows from the definitions and assumptions it uses.
That matters because the output includes something others can check beyond a written explanation. OpenAI has published the formalization on GitHub.
However, a checked proof still needs to express the intended mathematical problem correctly. Its assumptions and dependencies also require examination. Formal verification and independent mathematical review address different parts of establishing a result. Lean’s verification guide
What remains unsettled?
The announcement should still be described as a claimed resolution, rather than an independently accepted result.
There are also questions about credit and provenance. OpenAI discusses concurrent work by Levent Alpöge and Tristan Buckmaster, acknowledges their priority on forced Euler, and says it cannot rule out a contribution to model improvement from de-identified product usage. The correctness of a proof would not, by itself, settle those questions. OpenAI’s account
OpenAI also says it does not intend to claim the Millennium Prize.
Why this is worth watching
If the result holds, its significance extends beyond fluid mechanics. It would be evidence that a coordinated AI system can contribute to resolving a major open problem and produce a formal artifact for others to examine.
For developers, the interesting combination is sustained exploration, shared intermediate results, and a separate checking process. How much of that can become practical at smaller budgets remains an open question.
For now, there is a substantial mathematical claim on the table, a published proof to investigate, and a research process worth understanding. That is already plenty to take in.
Top comments (0)