Did AI solve Navier-Stokes?

Over roughly twelve hours on the 7th and 8th of September, two announcements landed. Just before midnight on Monday, Tristan Buckmaster of New York University published a statement describing work with Levent Alpöge, along with three preprints and Lean formalizations. On Tuesday morning, OpenAI announced that a coordinated system of about 10,000 agents, running on an internal model, had produced a proof that the three-dimensional Navier-Stokes equations develop a singularity in finite time, and said it resolved a Millennium Prize Problem.

What followed was a priority dispute, and the dispute is the part that travelled. I am going to leave almost all of it alone, because the interesting question is not who talked to whom. It is narrower and it is answerable from documents anyone can download: what would count as solving this, what has actually been proven, and what has not.

The problem is four statements

The Clay Institute's official description was written by Charles Fefferman of Princeton. It is six pages, it is a free PDF, and it does something most coverage does not mention: rather than pose one question, it offers four, and asks for a proof of any one of them.

Two of them say the equations behave. Statement (A) covers three-dimensional space, statement (B) covers the periodic case, and both carry the same restriction, in Fefferman's words: "Take f(x, t) to be identically zero." No external force at all. Smooth initial data, positive viscosity, and a demand that the solution stay smooth forever.

Two of them say the equations break. Statement (C) is the one that matters here, so here it is close to verbatim. Take viscosity positive and dimension three. Then there exist a smooth, divergence-free initial velocity field on three-dimensional space and a smooth force on that space for all positive time, both satisfying the decay conditions the paper sets out, for which no smooth finite-energy solution exists.

Read that carefully, because it settles a claim I have seen made confidently in both directions this week. The breakdown half of the Millennium Prize problem explicitly permits an external force. It has to be smooth and it has to decay, and subject to that, building a force that drives a smooth fluid into a singularity in finite time is a legitimate route to the prize. Anyone telling you that a forced blowup is automatically disqualified has not read statement (C). Anyone telling you that the forced and unforced problems are the same problem has not read statement (A).

So the forcing term is not a loophole. It is a door, and it is the door both teams were running at.

What the downloadable papers prove

Three preprints went up on Buckmaster's university page. I downloaded all three and read their statements of results. Their titles are the most useful summary anyone has written of this story:

Blowup for the Euler equations with smooth forcing. Blowup for the Boussinesq equations with smooth forcing. Extending the Córdoba-Martínez-Zoroa IPM blow-up to uniformly space-time smooth forcing.

Three equations. The incompressible porous medium equation on the two-dimensional torus, the inviscid Boussinesq system on the plane, and the three-dimensional incompressible Euler equations. Each result is a genuine, hard, forced finite-time blowup, and the Euler one in particular is the kind of thing people have been chasing for decades: a singularity on all of three-dimensional space, no boundary to blame it on, with a force that stays smooth in space and time right up to and including the blowup time.

None of the three is the Navier-Stokes equation.

And this is not a technicality I am imposing from outside. Fefferman addresses it directly in the official description, one sentence after listing the four statements: these problems "are also open and very important for the Euler equations (ν = 0), although the Euler equation is not on the Clay Institute's list of prize problems."

The prize rules make the same point in legal language. A paper that does not address the specific mathematical questions in the official description will not be considered a solution, in the rules' phrasing, "even if it addresses closely related scientific questions." Euler is the most closely related scientific question there is. It is still not the problem.

The difference is one term, and it is the whole difficulty

Euler is Navier-Stokes with the viscosity set to zero. One term, the Laplacian multiplied by ν, and deleting it changes the character of the equation completely. Viscosity is the mechanism that smooths a fluid out, and a blowup proof is an argument that something gets infinitely rough in finite time. Removing the smoothing removes the thing your construction has to defeat. As Fefferman put it to Quanta, in models with a boundary, a singularity tells you the fluid did it in cooperation with the wall, and without a boundary "it's the fluid doing the crazy stuff." The same reasoning applies to friction. With viscosity switched off, you have taken away the equation's defence.

Which brings me to the word that is missing from every headline I read, and which is sitting in plain sight inside the papers.

Hypodissipative

In the Boussinesq preprint, Alpöge and Buckmaster include a short section titled "AI statement." In it they mention, in passing, a further writeup they produced "for hypodissipative Navier-Stokes." Quanta describes the same object as an unverified proof of blowup "for a somewhat easier version of Navier-Stokes."

Hypodissipative means the viscous term has been weakened. Instead of the honest Laplacian, you use a fractional power of it, with the exponent small enough that the dissipation is much feebler than real friction. It is a standard and respectable tool: you dial the difficulty down until the problem becomes tractable, prove the result there, and then work on closing the gap. What it is not is Navier-Stokes. Fefferman's four statements all require ν > 0 multiplying the full Laplacian.

There is a further detail here that reframes the whole week, and I only found it because the Euler preprint's reference list is careful. Forced blowup for hypodissipative Navier-Stokes is not new and is not AI-derived. Diego Córdoba, Luis Martínez-Zoroa and Fan Zheng published exactly that result in the Archive for Rational Mechanics and Analysis in May 2026, in a paper whose title states the regularity class of the force it needs. That is a peer-reviewed, human-authored result sitting in the literature four months before this week's announcements.

So the ladder, as of today, reads roughly: forced blowup for IPM, done. Forced blowup for Boussinesq, done. Forced blowup for three-dimensional Euler, done, Lean-formalized. Forced blowup for hypodissipative Navier-Stokes, published in a journal in May, and separately claimed again this week without formal verification. Forced blowup for actual Navier-Stokes, claimed by OpenAI, proof not public. Unforced blowup, statement (A) or (B) territory, nobody.

Terence Tao, writing about the three preprints the day before the OpenAI announcement, put the status in one sentence: the authors "do not quite achieve these goals yet," though they have made enough of a breakthrough "that it looks very feasible to complete these goals in the near future." That is a considerably more precise statement than "AI solved Navier-Stokes," and it came from someone who had spoken to one of the authors on the phone.

What the AI actually did, per the people who used it

This is the part of the story I care about most, and the primary source for it is unusually good, because the authors wrote a section about it and put it in the paper.

They say they used Claude and Codex to iterate on the proof, that they had a first blowup solution on 15 August 2026 and had it Lean-verified on 22 August. They describe what they fed the models: ideas from their own prior joint work on IPM blowup following Córdoba and Martínez-Zoroa, other work of theirs and others, and iteration on various ansätze. Then this, about the output:

The first writeup that we produced iterating with Claude was, in our opinion, the worst writeup we had ever seen in the history of mathematics (topped soon after by the writeups for 3d Euler and then for hypodissipative Navier-Stokes). It was then our task to make a presentable and understandable writeup

Buckmaster said the same thing more bluntly in his announcement statement, calling one of the three released papers something that "can only be described as AI slop. I am sorry for this."

Now hold that against what the papers say about where the idea came from. The Boussinesq paper describes itself as developing a program initiated by Córdoba and Martínez-Zoroa, "whose groundbreaking multiscale constructions provide its principal intellectual foundation," and then states plainly: "We believe that the primary intellectual credit for the underlying strategy belongs to them."

That strategy is the actual mathematics. You build the solution in layers, each layer a well-behaved solution in its own right, each one adding a faster, finer oscillation that grows as you approach the blowup time, and you arrange the whole infinite cascade so the accumulated forcing stays smooth even though the solution does not. Córdoba and Martínez-Zoroa got the cascade to produce a singularity years ago. The step that had not been taken was making the forcing come out smooth as well. That step is what both AI-assisted efforts appear to have closed.

Fefferman, asked by Quanta who deserves credit, said he was thrilled the problem was solved, and that the heroes of the story are Córdoba and Martínez-Zoroa. Buckmaster, in his own announcement, wrote: "Let me make plain what I have said to colleagues in private: in view of this body of work, I believe Luis Martínez-Zoroa deserves a Fields Medal." Martínez-Zoroa, for his part, does not use AI much. His adviser Córdoba's line to Quanta is the best sentence in the whole affair: "I don't use AI: I have Luis."

So the honest shape of what happened is not a machine solving a famous problem from nothing. It is a human research program, unusual and unfashionable, developed over years by two people working analytically while the rest of the field went computational, which reached a point where the remaining gap was a very large amount of technically brutal but conceptually bounded work. That is precisely the shape of problem current models are good at. They were pointed at it by people who knew exactly where to point them, and the output needed weeks of human rewriting before another human could read it.

Lean proves the statement you wrote, not the statement you meant

Both efforts lean heavily, in the marketing sense, on Lean. Formal verification is genuinely strong evidence and I do not want to wave it away. A Lean-checked proof is not going to contain the kind of subtle gap that has killed famous claims before.

But it certifies a specific thing: that a particular formal statement follows from the axioms. It says nothing about whether that formal statement is the problem. Quanta names this directly, calling the crucial remaining human job the work of guaranteeing that the statement shown true in Lean is logically equivalent to what the mathematicians set out to prove.

For this problem that check is not a formality, and everything above is why. The gap between "blowup for Euler" and "blowup for Navier-Stokes" is one term. The gap between "hypodissipative" and "dissipative" is one exponent. The gap between statement (C) and statement (A) is whether a function is allowed to be nonzero. Each of those is a small edit to a formal statement and an enormous change in what has been proven. A Lean file cannot tell you which side of those lines it is on. A person has to read the theorem statement and compare it, line by line, to Fefferman's four pages.

As I write this, OpenAI's proof is not public, so nobody outside the company can perform that comparison. The description that has circulated, a smooth fluid initially at rest, a smooth applied force, finite energy throughout, and a singularity in finite time, does map onto the shape of statement (C). If the proof exists, holds, and the force satisfies the decay conditions in equation (5) of the official description, then it is a resolution of the Navier-Stokes Millennium Prize problem in the breakdown direction. That is a real and enormous if, and it is not resolvable by press release.

The clock nobody mentioned

Here is the cleanest answer to "has AI won a million dollars," and it comes from a four-page rules document on the Clay Institute's website that takes ten minutes to read.

A prize may be awarded only if four things hold. The proposed solution has been published by a "Qualifying Outlet." At least two years have elapsed since that publication. It has achieved general acceptance in the global mathematics community. And it has satisfactorily answered the questions raised by the official problem description.

A Qualifying Outlet is a refereed mathematics publication of worldwide repute, and the rules disqualify anything lacking a named and contactable editorial board, an editor able to identify an appropriate referee, a published refereeing process, or inclusion in MathSciNet. A preprint on a university web page is not one. A company blog post is not one. Neither is a Lean repository.

Then the two-year clock, stated twice for emphasis: the proposed solution "must survive rigorous examination by the global mathematics community for a minimum of two (2) years," and only then does the Institute decide whether detailed consideration is merited, at which point it convenes a committee of at least three people, two of them experts in the area.

Nothing announced this week has been submitted to a journal, let alone published in one. The earliest any of it could clear the waiting period is late 2028, and the clock starts at publication, not at announcement. So the answer to whether AI has won a Millennium Prize is no, and it is not a close call or a matter of opinion. It is a calendar.

One more clause deserves attention, because it is doing quiet work. The rules say the Institute "will pay special attention to the question of whether a Prize solution depends crucially on insights published prior to the solution under consideration," and that it may recognize such prior work in the citation or recommend including its author in the award. Fefferman's remark about heroes is not just sentiment, then. It describes a provision of the rules, and the multiscale cascade is about as clear a case of a crucial prior insight as the clause is ever likely to see.

Why an electronic warfare officer reads it this way

My own research background is microwave spectroscopy, not fluid dynamics, and I am not going to pretend to referee a 112-page blowup construction. What I can speak to is the habit that makes this story legible, and it comes from the other half of my career.

In electronic warfare you learn, quickly and sometimes expensively, to separate a demonstration from a capability. A jammer that defeats a link in a test range where you control the waveform, the geometry, and the power budget has demonstrated something real. It has not demonstrated that it works against that link. The difference lives entirely in the conditions you gave yourself, and the conditions are always in the fine print, never in the briefing slide. The discipline is to read the assumptions before the result, every time, because the result is written to be quotable and the assumptions are written to be accurate.

A forcing term is exactly that kind of condition. So is a fractional exponent on a dissipation operator. So is deleting viscosity. None of them is cheating, all of them are how hard problems get taken apart, and every one of them is a knob that was turned before the proof started. The papers say which knobs, in their titles and abstracts, in plain language. The headlines dropped all of them.

What I am not claiming

I am not saying OpenAI's result is wrong. I have not seen it, and neither has anyone else outside the company, which is the actual problem with assessing it. If it is what the description suggests, it is a major result that would settle the breakdown half of the problem.

I am not saying the AI contribution was trivial. Closing the smooth-forcing gap in the cascade is real work, and producing a Lean formalization of a construction this size is an achievement in itself. That the first drafts were unreadable is a statement about presentation, not about correctness.

I am also not adjudicating the priority dispute. Different parties are telling different stories about who learned what and when, the relevant evidence is private, and nothing in this report depends on how it comes out.

What I am saying is that four sentences in a freely available PDF define this problem, one more sentence in the same PDF removes Euler from the list, and four pages of rules say the prize cannot be awarded for at least two years after a journal publishes something. Every headline this week could have been checked against those documents in under an hour. The thing worth keeping is not the verdict. It is that for the biggest mathematical claim of the year, the official criteria were public, free, short, and almost entirely unread.