Navier–Stokes: what OpenAI actually proved

The headline in September 2026 said an AI had solved one of the seven million-dollar Millennium Prize problems. The truth is narrower and, I think, more interesting: a machine-checked proof that the equations can break down in finite time when you push them with a force — the softer side of the problem — delivered by ten thousand agents in eighty-eight hours, and immediately swallowed by a fight over who deserved the credit. The theorem is real. What it tells us about the next decade of mathematics is bigger than the theorem.

AI use : 25% — framing and editorial direction from the author; research, drafting and prose assisted by AI, full human review.

The claim

On 8 September 2026, OpenAI published a note titled “On the Navier–Stokes Millennium Prize Problem.” It reported that an unreleased internal model — described as significantly more capable than the GPT-6 Astra system — had been run as roughly ten thousand coordinating agents in parallel for about eighty-eight hours, and had produced a proof that a three-dimensional fluid, starting from rest and pushed by a smooth external force while keeping finite energy throughout, develops a singularity in finite time. Crucially, the argument was not just written in prose: it was formalised and checked in Lean, a proof assistant that mechanically verifies every logical step. OpenAI framed the result as establishing statements C and D of the official problem, and — this matters — said it would not claim the one-million-dollar prize.

To see why a company would announce a Millennium-problem proof and in the same breath decline the million dollars, you have to know what the problem actually asks.

The equations, and the four statements

The Navier–Stokes equations describe how a fluid's velocity field evolves: inertia carries the fluid along, pressure keeps it incompressible, and viscosity — internal friction — smooths out sharp gradients. The open question is deceptively physical. If you start a fluid off smooth, with finite energy and no external forcing, does it stay smooth forever — or can the velocity somewhere run to infinity in finite time (a “blow-up,” or singularity)? Nobody has ever produced a real fluid that blows up, and nobody has ever proved one cannot. That gap is the Millennium problem.

Charles Fefferman's official statement for the Clay Mathematics Institute splits it into four claims. Two are positive and unforced: (A) smooth data on all of space stays smooth forever, and (B) the same on a periodic box. Two are negative and permit a forcing term: (C) there exists smooth data and a smooth force on space for which the solution breaks down, and (D) the same on the box. Proving any one of the four resolves the problem.

Here is the whole subtlety. The version everyone has in mind when they say “the Navier–Stokes problem” is (A): the pure, unforced fluid, left to its own devices. Statements (C) and (D) let you add a tailored external force — you are allowed to reach in and push the fluid exactly where it hurts. A forced blow-up is a genuinely hard theorem, but it is the softer target, because some of the singularity can be smuggled in through the force. And it is harder than it sounds precisely because viscosity is fighting you the whole way: friction wants to dissipate the energy you are trying to concentrate. Forcing a viscous fluid to blow up in finite time is a real achievement. It is not the same thing as showing that an unforced fluid — the honest problem, statement (A) — ever does. That one remains completely untouched.

What was new — and what was not

This result did not fall out of the sky, and OpenAI's own account makes that clear. The “forcing” strategy for manufacturing singularities was developed by Diego Córdoba and Luis Martínez-Zoroa. In mid-August 2026, the mathematicians Tristan Buckmaster (NYU) and Levent Alpöge extended it to prove finite-time blow-up for the Euler equations — the inviscid, frictionless idealisation, where there is no viscosity to fight. OpenAI's contribution was to carry the same line of attack across to the full viscous Navier–Stokes equations, and to formalise the whole thing in Lean. So the conceptual lineage is human and recent; the machine's role was to push a known strategy through a much harder, fully-verified construction at a speed no human team could match.

And notice what has not happened. As of this writing, the Clay Institute still lists Navier–Stokes among its unsolved problems. A press release is not a Millennium Prize: Clay's rules require publication in a refereed venue, a two-year waiting period, and acceptance by the mathematical community before anything is called solved. OpenAI declining the prize is partly an acknowledgement of that process — and partly, one suspects, an acknowledgement that a forced blow-up is not the trophy the public thinks it is.

The part that is not in dispute: Lean

Strip away the noise and one fact stands on solid ground: the proof was checked by a machine. A Lean-verified proof is correct in the same sense that a program which compiles is syntactically valid — a mechanical, exhaustive verifier examined every inference and found no gap. This is a genuinely different epistemic situation from the usual one. When Vinay Deolalikar circulated a claimed proof that P ≠ NP in 2010, adjudicating it meant dozens of specialists reading for weeks — and it did not survive. A human proof is an argument you must be persuaded to trust. A Lean-checked proof is a claim that has already been checked.

This is the same closed loop that made code and formal mathematics the fastest-moving corners of AI, and it is worth being explicit about the mechanism. Where a task has a cheap, exact verifier — a compiler, a proof assistant, or, in the case of the Jacobian Conjecture, a determinant anyone can recompute — a model can propose a million candidate steps and keep only the ones that pass, with no human in the loop and no trust required. Verification is cheap; only the search is hard, which is exactly the asymmetry P vs NP is about. Ten thousand agents for eighty-eight hours is what “turning the crank” looks like once the crank exists. Give mathematics a mechanical verifier and it becomes a domain machines can saturate.

The part that is in dispute: credit

If the correctness is settled, almost nothing else is. The announcement set off an ugly and very public fight, and the details are contested, so take them as allegations rather than findings.

1. The pivot. Around 1 September, OpenAI researchers reportedly turned to Navier–Stokes after hearing that Buckmaster and Alpöge had cracked a version of the forced problem — using, as it happens, a rival lab's models.
2. The call. OpenAI asked Buckmaster for a call on 3 September; on the 6th, he says, he learned during that call that OpenAI was about to announce a proof by the same line of attack he and Alpöge had used.
3. The accusations. Buckmaster alleged the company might have drawn on his private, unpublished research stored inside a coding tool; that he was asked to write the work up as sole author while leaving Alpöge off; and that when he threatened to go public he was told, “Why would you ruin your career?”
4. The denial. OpenAI's Sébastien Bubeck publicly rejected the allegations as “false and inflammatory.” The company's note was updated to credit both mathematicians for concurrent work on the forced problem and to offer recognition of their priority.

Whatever the resolution, the shape is telling: the machine settled the mathematics in eighty-eight hours, and the humans have been arguing about the credit ever since.

Tao's lament

The most interesting reaction came from Terence Tao, who has spent years mapping precisely this terrain — including his own work on finite-time blow-up for modified fluid models, and a note published days earlier on blow-up with smooth forcing for related equations. His unease was not about whether the theorem is true. It was about what the mode of production costs. Indiscriminate AI mathematics, he suggested, is like “watching a movie and jumping straight from the first ten minutes to the last ten minutes; technically, all the plot lines are resolved, but most of the value of the experience was lost” — a practice that risks turning the subject into “a meaningless production quota ‘game.’”

That is the real argument, and it is not Luddism. The value of mathematics was never only the list of true statements; it was the understanding built while getting there — the structures, the analogies, the reasons a thing is true. A model that emits a Lean-checked proof hands you the fact and skips the understanding. For a compiler that is fine. For a human discipline whose entire point is comprehension, it is a genuine loss, and no amount of verification buys it back.

What it actually means

Two things, one narrow and one broad.

So: a real theorem, narrower than the headline, on the forced side of a problem whose honest form is still open — and, more durably, a clean demonstration that once a field acquires a mechanical verifier, machines will saturate it, and the hardest problems left standing are the human ones. That is the part worth watching.