On September 8, 2026, OpenAI published an analytical proof and a Lean formalization that, according to the company, solve the Navier–Stokes existence and smoothness problem through alternatives C and D in the Clay Mathematics Institute’s official formulation. The result constructs a three-dimensional incompressible solution that starts from rest, is subject to a smooth external force, and develops unbounded velocity in finite time while kinetic energy remains uniformly bounded. That is far more than an AI-generated conjecture, but it is not yet the same as definitive recognition by the mathematical community or by Clay.
The key is to separate three things that are often blended together in headlines: the published mathematical claim, the formal verification of a version of the theorem in Lean, and the independent validation needed for experts and institutions to accept that the formalization matches the problem exactly and that the full construction withstands scrutiny.
What OpenAI’s proof claims to demonstrate
The paper “Finite Time Blowup for Navier–Stokes” presents, for every positive viscosity, a smooth compactly supported force and velocity and pressure fields that remain smooth up to a singular time. The construction starts from zero initial velocity. As time approaches the singular instant, the maximum velocity norm becomes unbounded while the energy norm stays bounded.
In less technical terms, the construction describes a vortex that contracts and spins faster and faster. The challenge is not simply to choose an external force that also becomes infinite: the paper aims to make the fluid’s own nonlinear dynamics produce the growth while the residual force remains smooth. OpenAI says this mechanism establishes alternative C in the whole space and, because of compact support, alternative D in the periodic setting as well.
Why the external force does not automatically make the result irrelevant
An important source of confusion is treating “forced” as automatically meaning a different problem from the Millennium Prize formulation. Clay’s official statement allows a smooth external force satisfying regularity and decay conditions in alternatives C and D for breakdown. Therefore, if the published construction really satisfies all those hypotheses, using a smooth force does not disqualify the strategy.
This also means the result should not be made stronger than what was proved. It does not show that every smooth unforced flow develops singularities, nor that a real glass of water will reach infinite speed. The claim is existential: there is an admissible mathematical configuration in which a smooth solution cannot be continued globally under the formulation’s requirements.
What role does Lean play?
OpenAI published a repository containing Lean 4 certificates for the Navier–Stokes and Euler results. In a system such as Lean, a proof script is turned into a logical object that is checked by a small kernel. When compilation and checking succeed, the kernel accepts that the formal theorem follows from the definitions, imported theorems, and axioms declared in the environment.
This is a powerful safeguard against many kinds of mistakes in long proofs: unfinished goals, steps that do not follow from the assumptions, or hidden failures in tactics cannot simply pass as a valid proof once the final proof term is checked by the kernel. Lean’s own documentation, however, emphasizes a crucial boundary: the check has its intended meaning only if the formal statement correctly corresponds to the intended informal mathematical claim and if the definitions and dependencies mean what they are supposed to mean.
OpenAI’s repository also provides instructions for independent checking with Comparator, a tool that can rebuild and recheck the certificate in a more controlled environment and with external checkers. Making that material available makes reproducible audits easier, but providing a checking path is not the same as saying the whole mathematical community has already completed the audit.
The three layers of validation that should not be confused
| Layer | What it establishes | What still needs examination |
|---|---|---|
| Published analytical proof | There is a detailed mathematical construction with an explicit theorem and a chain of arguments. | Experts still need to review estimates, assumptions, corrections, limits, and possible gaps. |
| Lean formalization | The kernel can verify that the certificate derives the formal statement from the logical environment used. | Auditors must confirm that the formal statement, definitions, and dependencies exactly represent Clay’s conditions. |
| Mathematical and institutional recognition | It emerges when the result survives independent examination and gains broad acceptance. | Clay’s rules require publication in a qualifying outlet, at least two years, and general acceptance before any potential prize review. |
What the independent reaction lets us say now
Nature’s September 8 coverage treated the announcement as a claim of enormous importance, not as an editorial certification that the problem is already definitively closed. The report recorded positive initial reactions from mathematicians, including Clay Mathematics Institute president Martin Bridson and specialist Luis Martínez Zoroa. Those reactions show that the work is being taken seriously, but they do not replace detailed review.
That distinction matters because a 166-page proof accompanied by an extensive formalization can be plausible, impressive, and still be at the beginning of scrutiny. In mathematics, moving from “a proof has been published” to “the problem is accepted as solved” depends on experts being able to reconstruct, test, and compare the arguments independently.
Why the Clay Mathematics Institute does not decide this immediately
The Millennium Prize rules are deliberately slow. Clay does not accept a proposed solution for immediate direct evaluation. Before it will consider one, the solution must be published in a qualifying outlet, at least two years must have passed since that publication, and the solution must have achieved general acceptance in the global mathematics community. Only after that can the institute conduct its own examination.
OpenAI has said it does not intend to claim the US$1 million prize. Even so, the rules are useful for understanding the news status: mathematical correctness can be debated long before institutional recognition, and institutional recognition, by design, does not happen on announcement day.
So, was Navier–Stokes solved by AI?
The most precise answer as of September 9, 2026 is: OpenAI has presented a very substantial candidate solution, with a public analytical proof and a Lean formal certificate, claiming to resolve alternatives C and D of the official problem. If the correspondence between the formalized theorem and Clay’s formulation is correct and the arguments withstand independent scrutiny, this would constitute a resolution of the Millennium Prize Problem by a construction found by an AI system.
What cannot yet be stated without qualification is that the result has already received broad mathematical validation or Clay recognition. Lean greatly reduces the risk of certain logical errors inside the formalization, but it does not replace the human task of checking that what was formalized is exactly the relevant theorem, that the definitions carry the intended meaning, and that the result fully fits the rules of the original problem.
