An AI May Have Solved Navier-Stokes. Now Comes the Human Part

At some point during the first weekend of September, a vast artificial research operation appears to have found something generations of mathematicians had missed.

OpenAI says it assigned roughly 10,000 coordinated AI agents to the Navier-Stokes problem, one of the original seven Millennium Prize Problems. The agents reached a proposed resolution after about 88 hours. Lean formalization and verification took another 17 hours using GPT-6 Astra, according to the company.

The result arrived on September 8 as a 166-page analytical paper and a public repository of Lean code. If the construction survives scrutiny, AI will have played a decisive role in resolving a question left open by Jean Leray's work in 1934.

That “if” deserves care, but not because this resembles the usual spectacle of a chatbot inventing plausible-looking mathematics. On September 10, the Clay Mathematics Institute, which administers the prize, said Navier-Stokes had “apparently been settled.” The European Mathematical Society called the announcement a milestone and joined in celebrating the achievement.

Clay still lists the problem as Active. Its rules require publication through a qualifying outlet, general acceptance by mathematicians and at least two years of examination before it will consider a proposed solution. OpenAI says it does not intend to claim the $1 million prize.

So what did the AI actually produce, and why are humans still needed?

A vortex that gets faster as it disappears

The Navier-Stokes equations describe how fluids move. Scientists and engineers use them constantly, but their mathematical foundations contain an unnerving gap: nobody has known whether a smooth three-dimensional solution must remain smooth forever or can develop a singularity in finite time.

A singularity is not merely a particularly messy patch of turbulence. In the result claimed by OpenAI, the fluid's maximum velocity grows without bound as time approaches a particular instant.

The construction begins with fluid at rest. A specially designed external force sets it moving, producing a vortex that spirals inward and stretches along its axis. As the critical time approaches, the core becomes thinner and dramatically faster.

That creates an apparent paradox. If part of the fluid is moving arbitrarily fast, shouldn't its energy also become infinite?

Not necessarily. Kinetic energy depends not only on speed but on how much fluid is moving at that speed. The fast-moving core occupies an ever-smaller volume. In OpenAI's construction, it shrinks quickly enough that its contribution to the kinetic energy tends toward zero even as its peak speed grows without limit. An increasingly violent event is squeezed into an increasingly tiny region.

Viscosity should resist this concentration by smoothing the flow. The proposed vortex is arranged so that inward transport continues spinning it up while viscosity transfers momentum outward. Oscillatory pulses around the core provide additional momentum flux, canceling terms that would otherwise make the required external force singular too.

That last detail is essential. For a sufficiently complicated velocity field, one could simply define whatever force makes the equation balance. That would prove little if the force itself became infinite at the crucial moment. The difficult feat is to make the velocity blow up while the applied force remains smooth in space and time.

The paper claims to do exactly that for every positive viscosity. In its whole-space result, fluid that begins at rest is driven by a smooth, compactly supported force; its total kinetic energy stays bounded while its maximum velocity becomes unbounded as the normalized time approaches 1.

Yes, the force is allowed

The external force has prompted claims that OpenAI solved an easier or different problem. The official formulation written by Charles Fefferman, however, provides four possible routes.

Alternatives A and B ask for global smoothness without forcing. Alternatives C and D permit a smooth force and ask for a counterexample in ordinary three-dimensional space or on a periodic three-dimensional torus. OpenAI's paper targets C and D.

The force makes this an extremely engineered example. The proposed result does not mean a glass of water or a weather system is likely to accelerate toward infinite speed, and it does not suddenly invalidate aircraft simulations. Navier-Stokes remains extraordinarily useful in the regimes where engineers apply it.

But forced blowup is not a technical loophole. It is one of the outcomes Clay explicitly agreed would settle the stated problem.

What Lean proves, and what it doesn't

A conventional proof this long would be terrifying to referee. One hidden sign error or unjustified estimate could undermine the construction.

Lean changes the nature of that check. The theorem, definitions and logical steps are converted into proof terms that Lean's small kernel can verify. High-level automation may create those terms, but the kernel decides whether they establish the encoded theorem. OpenAI also provides instructions for checking exported results with separate Comparator tooling.

That is much stronger evidence than a plausible-looking PDF. It does not close every question.

A formal proof can flawlessly establish the wrong statement if its definitions omit a required condition. Reviewers must confirm that the Lean theorem matches alternatives C and D, that it includes the required smoothness and support conditions, and that the enormous informal paper describes the same construction as the formal artifact.

Humans also want more than a certificate saying the conclusion follows. They want to understand why it follows: which ideas are essential, which mechanisms generalize and what new mathematics can be built from them. A proof can be logically airtight yet remain intellectually opaque.

Clay's unusually positive statement is an encouraging sign. It is not a substitute for specialists reading, reconstructing and explaining the argument. A derivative preprint that appeared shortly after OpenAI's announcement was withdrawn on September 11 and did not independently verify the proof. There is not yet a publicly identified, complete independent audit.

The other problem has no proof assistant

Even if Lean settles the internal logic, it cannot decide who deserves credit.

OpenAI's construction did not emerge from nothing. Its paper cites a line of forced-singularity research developed by Diego Córdoba, Luis Martínez-Zoroa, Fan Zheng and collaborators. The EMS said OpenAI's strategy is closely related to that work and emphasized that the result rests on decades of human mathematics.

Meanwhile, NYU mathematician Tristan Buckmaster and Levent Alpöge, a mathematician employed by Anthropic, had been using several AI systems to push the same broad program forward. In a signed statement, Buckmaster says they obtained smooth-forcing blowup results for the Boussinesq and Euler equations on August 15 and verified them in Lean on August 22. They released related results on September 7, one day before OpenAI's announcement.

That day, Terence Tao explained that their method had a high likelihood of extending to Navier-Stokes.

OpenAI says it began testing its new internal model against the open Millennium Problems on September 1 after hearing rumors that major problems had been resolved. It says its agents completed the Navier-Stokes construction on September 5 and the Lean formalization on September 6.

Buckmaster questioned whether knowledge of his collaboration had directed OpenAI toward the forced route. He also raised concerns about private work entered into Codex and alleged that OpenAI mathematician Sébastien Bubeck twice sought to exclude Alpöge from a proposed paper presenting OpenAI's result because Alpöge works for Anthropic.

Bubeck gave a narrower account of that authorship discussion. He denied asking to remove Alpöge from authorship of Alpöge's own work. He said the proposal concerned Buckmaster becoming lead author of a rewrite of OpenAI's proof and that he considered it inappropriate for an Anthropic employee to author OpenAI's work. That does not resolve Buckmaster's contrary account of what was said during the calls.

In a September 10 update, OpenAI said an internal investigation established that Buckmaster's Codex prompts from the preceding two months could not have influenced the system, including through training. The company also said the proofs differ significantly. The public evidence does not establish that OpenAI used the pair's private research, but outsiders cannot independently audit the internal model or the investigation.

What is established is more complicated. A rumor about outside progress helped trigger an industrial-scale attack. The successful construction belongs to a published research lineage. And a laboratory with an inaccessible model and enormous computational resources crossed the finish line before mathematicians working nearby could finish presenting their own related results.

That arrangement may become familiar. Researchers will use commercial models as collaborators while the companies operating those models possess greater tools, resources and visibility than any individual customer. Traditional ideas of independent discovery and priority were not designed for this relationship.

Lean can check whether a conclusion follows from premises. It cannot decide whether a mathematical explanation is good, whether access to a private model was fair or how recognition should be divided among a machine, the people who deployed it and the people whose earlier ideas made its search productive.

The Navier-Stokes question may finally have an answer. The harder work now is turning that answer into human knowledge, and deciding whose knowledge it is.