OpenAI's Navier-Stokes Proof: What Was Actually Proved
OpenAI says an AI cracked a Millennium Prize Problem. The Clay rules do allow a forcing term, so here's what the proof settles and what stays open.

On 8 September 2026, OpenAI published a page called On the Navier–Stokes Millennium Prize Problem and said an internal model had produced a proof. Within a day the reaction had split cleanly in two. One half called it the biggest mathematical result of the decade. The other half called it a technicality.
Both halves are looking at the same claim. They disagree about one letter in the equation: f, the forcing term.
That letter is worth understanding, because the fine print here is more interesting than either headline.
What "blows up" means
The Navier-Stokes equations describe how a fluid moves. You hand them a smooth starting velocity, and they tell you the velocity at every later moment. In two dimensions we've known since Ladyzhenskaya's work that smooth starts stay smooth forever. In three dimensions nobody knows.
A blow-up, or singularity, is a solution where some quantity runs off to infinity in finite time. For Navier-Stokes that quantity is the velocity itself. At time T the maths says a speck of fluid is moving infinitely fast.
Real water does not do this. So a blow-up wouldn't mean fluids are broken. It would mean the equations stop describing fluids at that instant, and every simulation built on them has a horizon nobody has mapped.
That is the open question. Does the model break, or does it hold forever?
Clay's four statements, and the one everybody skipped
The Clay Mathematics Institute put Navier-Stokes on its list of seven Millennium Prize Problems in 2000, each worth a million dollars. Charles Fefferman wrote the official problem description. He asks for a proof of any one of four statements, and this is where the argument lives.
Statements (A) and (B) are the ones people quote. Existence and smoothness, on all of space and on the periodic torus. Both contain the same instruction in the setup: "Take f(x,t) to be identically zero." No external force. Just the fluid, left alone.
Statements (C) and (D) are the breakdown half, and they are written differently. Fefferman asks you to show "there exist a smooth, divergence-free vector field u°(x) on R³ and a smooth f(x,t) on R³ × [0,∞), satisfying (4), (5), for which there exist no solutions."
A forcing term is written into the breakdown half of the problem, by the person who wrote the problem. This is the part most coverage dropped. Pushing on the fluid isn't a loophole somebody discovered in the rules. It is in the text of the rules.
There is a real constraint on it, though. Conditions (4) and (5) require f to stay smooth and to decay fast in both space and time, faster than any polynomial. A force that quietly goes singular itself, and drags the fluid along with it, is ruled out. You have to break the fluid with a force that never breaks.
(A) and (C) are not opposites
This is the bit worth sitting with. (A) says every unforced smooth start stays smooth forever. (C) says some forced smooth start breaks down. Both can be true at the same time, because they are asking about different equations. Clay hands you two separate questions and pays out for either one.
What OpenAI says it has
The claim, as reported from OpenAI's announcement, is a smooth fluid starting at rest, under a smooth external force, developing a singularity in finite time while its total energy stays finite. The mechanism is described as inward-spiralling vortices. OpenAI says this establishes statement (C), and also (D).
The production numbers, per Quanta, are the part that got screenshotted:
| What | Reported figure |
|---|---|
| Agents running in parallel | about 10,000 |
| Wall-clock time to the proof | 88 hours |
| Messages exchanged between agents | roughly 5 million |
| Extra time to formalise in Lean | 17 hours |
| Model | only described as "significantly more capable than GPT-6 Astra" |
Two things OpenAI did not do. It did not claim the million dollars. And it did not publish the proof. As of writing, nobody outside the company has read those roughly 100 pages. Buckmaster, the mathematician closest to the work, confirmed he hadn't seen it.
The twelve hours before
The announcement did not land in an empty room. Late on 7 September, Tristan Buckmaster at NYU and Levent Alpöge at Anthropic posted three preprints: finite-time blow-up with smooth forcing for the incompressible porous medium equation, for 2D Boussinesq, and for 3D incompressible Euler. They shipped Lean formalisations alongside them, in a public repository with separate Euler and Boussinesq blow-up modules.
Terence Tao wrote the results up the same day and was careful about scope. Euler is not on the Clay list. Boussinesq and IPM are not either. His read on where this leads: "it should be possible to construct smooth initial data and smooth forcing term that would make these equations develop singularities in finite time; and it should even be possible to do without the forcing term."
Both efforts stand on the same foundation, and it is a human one. Diego Córdoba and Luis Martínez-Zoroa built the technique between 2021 and 2023, a way of stacking high-frequency corrections that exploit instabilities in the linearised equations. Fefferman, who wrote the problem statement, told Quanta he "was thrilled that the problem was solved" and then pointed at them: "The heroes of the story...are Córdoba and Martínez-Zoroa." Buckmaster went further and said Martínez-Zoroa deserves a Fields Medal.
Buckmaster also gave the most quotable line about working this way. The first proof his models generated was, in his words, "the most horrendous I have ever read."
There is an active credit dispute layered on top. Buckmaster alleges OpenAI learned of his unpublished collaboration and raced a competing result out. OpenAI's Sébastien Bubeck denies it: "We did not use their prompt or proofs to prompt our models." That fight matters, and it deserves its own post rather than a paragraph here.
So is it solved?
Depends which question you meant, and this is the honest answer rather than a hedge.
The prize statement. If the proof holds and the forcing term satisfies conditions (4) and (5), statement (C) is exactly what Fefferman asked for. Not a workaround. The thing he wrote down.
The question people actually care about. Whether Navier-Stokes left alone, with no external force, breaks by itself. That is (A) and (B), and it is untouched. Tao thinks it should be reachable. Nobody has reached it.
The prize itself. Clay's rules require publication in a peer-reviewed journal of worldwide repute, followed by two years of general acceptance in the mathematics community, judged by the Scientific Advisory Board. In 26 years exactly one Millennium Prize has been awarded, for the Poincaré conjecture, and Grigori Perelman turned the money down. A press call starts that clock at zero.
Quick check
OpenAI's claimed proof uses an external forcing term. What does that mean for the Clay problem?
Reading the next claim like this one
You will get another one of these. Some lab will announce that a model solved something big, and the announcement will arrive before the artifact. Three questions sort the signal from the press release, and none of them need a maths degree.
What is the exact statement? Not the headline. The theorem. "Navier-Stokes blows up" and "forced Navier-Stokes blows up under conditions (4) and (5)" are different sentences with different consequences, and only one of them was on offer here.
What is the checkable artifact? Buckmaster and Alpöge shipped Lean files anyone can run. OpenAI described a result on a call. Lean is the interesting move, because a formal proof assistant checks every step mechanically. That matters more, not less, when the author is a model that has a documented habit of producing confident wrong output. This is the same instinct behind writing tests before you trust code, scaled up to mathematics.
Who checked it, and are they independent? A claim isn't a result until somebody outside the building can verify it.
That last one is the whole story of this week. It is also why OpenAI's own GPT-6 Astra scorecard was worth reading closely rather than taking at headline value. The pattern repeats.
What to watch next
Watch for the preprint. If OpenAI posts the 100 pages and the Lean formalisation, mathematicians can check whether the forcing term really satisfies Fefferman's decay conditions, and this stops being a debate about a press release.
Watch the unforced case. That is the actual prize, in the sense most people mean it, and Tao is on record saying he expects it to fall.
And watch how the credit settles. The technique came from two mathematicians in Spain, the first public artifacts came from a professor and a researcher working nights, and the announcement came from a company that ran 10,000 agents at the problem for 88 hours. All three of those are part of how this got done.

Written by
Rhythm Bhiwani
Engineer and relentless builder, happiest reverse-engineering hard problems until they click.
Enjoyed this?
Tap the heart to leave some love.
Be the first to react
Comments
Join the conversation.
Loading comments…


