Spend 15 million dollars to win 1.

I spend my working hours trying to get a handful of agents to stop stepping on each other's toes. So when my timeline told me on Monday morning that ten thousand of them had spent a long weekend solving a Millennium Prize problem, my first reaction was not awe. It was a very specific and slightly petty question: what exactly was the prompt?

My second reaction was better. Before I read a single news article, I opened the five-page PDF that Charles Fefferman wrote for the Clay Mathematics Institute in the year 2000, the one that defines what “solving Navier–Stokes” legally means.[1] That turned out to be the correct order to read things in, and this whole post is essentially an argument for that order.

Here is the sentence everybody was arguing about on Monday: “OpenAI solved Navier–Stokes.” The sentence is doing three jobs at once, and only one of them is true in the way people assume.

1. A theorem was proved about the three-dimensional Navier–Stokes equations with a smooth external force, and a proof assistant checked it.
2. That theorem matches, clause for clause, one of the four alternatives in the official problem statement. Specifically alternative (C), and by a small extension alternative (D).
3. That alternative is the thing people mean when they say “the Navier–Stokes problem.”

The first claim is, as far as anyone can currently tell, correct. I cloned the Lean repository and I will show you what is in it. The second claim I can verify myself, because the problem statement is five pages long and the relevant clause is two sentences. The third claim is false, and it is false in a way that Fefferman anticipated twenty-six years ago when he wrote four alternatives instead of one.

So this is not a post about whether a million dollars changes hands. OpenAI has already said it will not ask for it.[2] This is a post about what a shrinking vortex, a gentle push, an energy budget, four hundred thousand lines of Lean, and one very bad month for a mathematician in New York actually add up to. I have kept the mathematics to the few lines that carry the story; everything else is in words.

The equations, in one paragraph and one balance sheet

You do not need to have seen a partial differential equation before to follow this. The Navier–Stokes equations are Newton's law, force equals mass times acceleration, written for every tiny parcel of water at once. In symbols:

Here \(u\) is the velocity of the water at each point, \(p\) is the pressure, \(\nu\) is the viscosity (how syrupy the fluid is), and \(f\) is any force applied from outside, like gravity or a stirring spoon. There is also a rule that the water cannot be compressed. The awkward piece is the term \((u\cdot\nabla)u\): the water carries itself around, so the velocity appears twice, multiplied by itself. That one self-referential term is the whole reason nobody has solved the problem in ninety years. Set the friction \(\nu\) to zero and you get the older Euler equations, which are easier to break.

One consequence of the equation matters more than any other for this story. Multiply through by the velocity and add up over all of space, and you get an energy balance:

Read it slowly. Energy can only go down through friction, and can only go up if something outside pushes. With no outside push, the total energy of the fluid can never increase. That is why the unforced problem feels like it should have a tame answer: the fluid has a fixed budget and friction taxes it constantly.

But the balance says nothing about where the energy sits. A tiny region can hold enormous speeds while holding almost no energy, the way a pinprick can carry huge pressure with little total force. That loophole is the shape of every singularity in this post.

Fefferman wrote four sentences

The Clay problem statement does not say “prove or disprove global regularity.” It asks for a proof of one of four statements. I am going to paraphrase them closely, and I want you to watch the force.[1]

Look at the third column. The two existence alternatives explicitly set the force to zero: “Take \(f(x,t)\) to be identically zero.” The two breakdown alternatives explicitly allow a force, as long as it is smooth and fades away far from the origin and late in time. A push that is smooth and simply switched off outside a bounded region of space and time satisfies that condition automatically.

This is the fact the whole week hinges on. The version of the problem that lives in most people's heads, “take smooth initial data, no external push, does the fluid ever blow up?”, is the breakdown question with \(f\equiv0\). It is not one of the four alternatives. Fefferman gave the solver, in his own words, “reasonable leeway” by allowing a smooth force in the breakdown direction. Almost every working analyst I have read this week says the same thing: they had mentally deleted that clause.[3][4] Buckmaster called the forced route “not the direction one arrives at in a few days by giving a model the problem statement.”[5]

OpenAI did not delete the clause. Neither, for years before them, did two mathematicians in Madrid.

What the 166 pages claim

The manuscript is titled “Finite Time Blowup for Navier–Stokes,” author line “OpenAI,” 166 pages.[6] Its main theorem, stripped of notation, says this.

In symbols, the two conditions that do the work are

Four things in that statement deserve a pause.

First, the fluid starts at rest. Everything that happens is caused by a finite, gentle push. A smooth push producing an infinite speed is a stranger claim than “some wild starting state blows up.”

Second, the theorem holds for every viscosity, thick or thin. The reason is a neat symmetry: if you have a blowup at viscosity one, you can shrink or stretch space and rescale the speeds, and the same recipe becomes a blowup at any other viscosity, at the same moment in time. One construction is therefore every construction.[6]

Third, alternative (C) says “no global solution exists,” not “here is a solution that blows up.” To get from the second to the first you need one more fact: any well-behaved solution with the same push and the same start would have to be the same solution, and so would blow up too. That is a standard uniqueness fact for these equations, but it is a step, and the Lean proof has to include it.

Fourth, because the whole flow lives inside a bounded box, you can copy the box side by side forever and get a periodic version. That is how (C) becomes (D).[6]

A vortex that eats its own width

Now the physics, which is the part I found genuinely beautiful, and which you can picture without any equations.

The flow is a vortex, a spinning column like the one above a bathtub drain. Water spirals inward toward the axis, spins faster as it gets closer, and squirts out along the axis in both directions so that it does not pile up. As the blowup moment approaches, the column gets thinner and thinner and spins faster and faster. And it gets thin in a lopsided way: its width shrinks faster than its height, so it becomes a needle.[6]

Why does the spin speed up? The same reason a figure skater speeds up when she pulls her arms in. A parcel of water moving inward keeps its angular momentum, so its speed around the axis must rise. Friction fights this by leaking spin outward, and the actual speed is the balance between the two.

Here is the one calculation I did on paper, and it is short. Write \(\tau\) for the time left before the blowup. The paper says the width of the needle shrinks like \(\sqrt{\tau}\), the height shrinks like \(\sqrt{\tau}\) too but a hair more slowly, and the speed grows like \(1/\sqrt{\tau}\), again with a hair extra. The energy inside the needle is roughly

ignoring the hairs. As \(\tau\) goes to zero, so does the energy. The fastest water in the universe lives in a needle so thin that its energy contribution vanishes. The energy balance from the first section is satisfied without complaint. That is the loophole, executed.

The “hair extra” is a fixed number the paper calls \(h\), and it is smaller than one percent. It is the margin by which spin beats friction in the core. Keep that in mind: the whole viscous proof lives inside a margin of under one percent, which is a fair one-line explanation of why Navier–Stokes took 166 pages and Euler took 57.

The force is a leftover

Now for the trick that makes the forced problem attackable at all. I think it is the single most important idea to take away from this week if you are not a fluids person.

Take any smooth velocity field you like, one you invented, one that never solved anything. Plug it into the left side of the Navier–Stokes equation and compute what is left over. Call that leftover \(f\):

Then your invented field solves the forced Navier–Stokes equations with force \(f\), automatically, by definition. You have not solved a differential equation. You have computed a leftover and given it a name.

So the forced blowup problem is not “start the fluid and watch what happens.” It is a design problem: invent a velocity field that blows up, then arrange that its leftover \(f\) is smooth and gentle, even at the moment of blowup. Each individual piece of the leftover explodes as the blowup approaches. The entire difficulty is making the explosions cancel. The paper says it plainly: the individual terms “can diverge, but we must arrange sufficient cancellation that their sum and all its derivatives extend smoothly through the singular time.”[6]

Contrast that with the unforced problem. There, \(f=0\) is a rule you cannot design around. You pick a starting state and you must follow the genuine, uncontrolled evolution all the way to the singularity. The forced problem lets you choose the path and pay for it with a push; the difficulty is keeping the bill smooth. The unforced problem gives you no credit card.

This framing is not OpenAI's. It is the program of Diego Córdoba and Luis Martínez-Zoroa, developed over several years in Madrid, and every party to this week's dispute agrees on that. Their idea, in Tao's description, is to build the flow in layers.[3] Start with a big, slow swirl. Add a smaller, faster ripple on top that is unstable in the big swirl, meaning a vanishingly small seed grows large on its own. Because it grows on its own, it costs almost no outside push. Add a still smaller ripple on top of that, and so on. The big scales shear the small scales into existence, each layer is the parent of the next, and the sum blows up while the total push stays gentle.

The hard part, and the reason this took from 2023 to 2026, was not the blowup. It was the adjective. Córdoba and Martínez-Zoroa's original 2023 singularity needed a push that was slightly rough, not smooth enough for Fefferman's fine print.[7] Every step since then has been about making the push smoother.

Alpöge and Buckmaster's August result is the rung directly beneath OpenAI's. They built a blowup for the Euler equations, no friction, driven by a push that is perfectly smooth in space and time right up to the moment of blowup, with the fluid's spin becoming infinite in exactly the way the classical theory says a real breakdown must.[8] It is 112 pages. It is Lean-verified. It is the same program, one rung down, and it was public on the evening of September 7.

Pulses that pay the momentum bill

Back to OpenAI's construction. The spinning needle balances itself in its own core. The trouble is the join: in a ring around the core, where the needle meets the calm outer fluid, the leftover force is not smooth. It is not even bounded. If you stopped here and called that leftover your push, you would have broken the rules.

The fix is to make the fluid supply the missing push itself. The construction adds a sequence of ripples in that ring, each wrapping all the way around, each living only briefly. A ripple that goes back and forth averages to zero motion, but it does not average to zero transport. Think of a crowd swaying: nobody ends up anywhere new, but if the people swaying outward are carrying more than the people swaying inward, stuff still moves outward on average. The paper's ripples are tuned so that their average transport of spin and of axial motion exactly supplies what the join was missing.[6] Two families of ripples are needed, because you need two independent directions of transport to hit an arbitrary target, and their strengths must both be positive, which constrains the shape of the needle itself.

Where do the ripples get their energy? From the spinning background. A ripple lying at the right angle to the shear gets fed by it and grows. But the same shear that feeds the ripple also tilts it, and a tilted ripple has shorter waves, and friction kills short waves faster than long ones. So each ripple grows, peaks, and dies, and it needs an outside push only for its vanishingly small birth and its vanishingly small death.[6]

The paper checks the arithmetic of this budget: the rate at which the shear feeds a ripple and the rate at which friction eats it are exactly the same size. That is not luck; it is the design. The ripples live precisely at the scale where feeding and eating compete evenly, so a small tilt is enough to flip the winner. Everything closes.

Why viscosity was the boss fight

If you only remember one technical thing from this post, remember this: without friction there is nothing eating the ripples. In the Euler version every seed grows forever, and the only question is keeping the push smooth as you stack layers. Alpöge and Buckmaster did that in August, and OpenAI's own 57-page Euler paper does something stronger still, which I will get to.

With friction, short waves die fast. A construction that stacks widely separated scales, which is the natural way to build a singularity out of layers, is exactly the construction friction punishes hardest. On September 8, Stan Palasek pointed out on Tao's blog that for the unforced Navier–Stokes problem, a route built through instabilities at widely separated scales runs into precisely this wall: friction eats the energy faster than the layers can grow.[9] Tao welcomed the observation and suggested a toy model to study it.

This is the honest version of “forcing makes it easier.” Forcing does not merely let you cheat by pushing. It lets you place every ripple at the knife-edge scale, seed it with a nudge so small friction has not had time to kill it, and top up the ledger with a smooth correction whenever it drifts. Without the force, the ledger has to balance itself while friction taxes it every step. Nobody has shown how to do that. OpenAI has not claimed to. Their own blog post says the unforced question remains open.[2]

What Lean did and did not check

I cloned the repository OpenAI released alongside the paper.[10] Here is what is in it.

The toolchain is Lean 4.34.0-rc2 with Mathlib. A recursive search of the two proof directories for sorry, axiom, and native_decide returns nothing; the only sorrys are the two placeholders in the challenge files, which is where they are supposed to be. The permitted axioms listed in the challenge configuration are the three standard ones, propext, Quot.sound, and Classical.choice.

Now the part that matters more than the line count. A proof assistant certifies that a formal statement follows from the axioms. It does not certify that the formal statement is the theorem you think it is. This is the gap that every careful commentator flagged this week, and it is a real gap.[11] OpenAI's answer to it is the Comparator setup, and it is a clever answer.

The challenge file is not written by OpenAI. It is copied, with a license header saying so, from Google DeepMind's Formal Conjectures project, which had already formalised Fefferman's four alternatives independently of any proof.[12] The relevant theorem, verbatim from the file I cloned, is:

/-- (C) Breakdown of Navier–Stokes solutions on ℝ³. -/
theorem navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) :
    ∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³),
    InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧
    ¬ (∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p) := by
  sorry

The Comparator tool then checks that OpenAI's proof module closes this exact statement, with these exact definitions, using only the permitted axioms. So the question “does the Lean theorem match Fefferman?” reduces to “does the Formal Conjectures encoding match Fefferman?”, which is a question about 472 lines that anyone can read in an afternoon, written by a third party before the proof existed.

I read them. The file spells out, in Lean's language, exactly what Fefferman wrote in English: the push must be smooth and fade away at large distances and late times; a “solution” must satisfy the equation at every point and every time, be incompressible, start from the given state, be smooth, and keep its total energy under one fixed bound forever. The periodic version also insists the pressure be periodic, which Fefferman added in a later correction. I could not find a way in which the Lean version asks for less than the prose does.

What the Lean certificate cannot tell you is whether the informal 166-page paper is a faithful narration of the formal proof, or whether the informal paper is readable, or whether it contains insight. Those are different questions and I will come back to them.

The other paper nobody is talking about

Sitting in the same repository, and in a second PDF that got a fraction of the attention, is a result that I think is mathematically at least as surprising as the headline.[13]

No force. Whole space. Smooth data. Compact support. Finite energy. This is the question people actually mean when they say “does Euler blow up,” and it has been open since Euler. The previous landmarks all carried an asterisk: Elgindi's 2021 singularity starts from data that is only slightly rough rather than perfectly smooth;[14] Chen and Hou's 2022 smooth-data blowup lives in a cylinder with a wall, and Fefferman himself explained to Quanta why a wall changes the meaning, since “without a boundary it's the fluid doing the crazy stuff.”[4][15] The unforced Euler paper is 57 pages, 1,839 Lean files, and the mechanism is different from the Navier–Stokes one: a shear at the origin stretches a small ripple, the stretched ripple becomes the shear for the next one, and the starting state is assembled from the sum of all those ripples.[13]

Two more things sit next to it. Buckmaster's statement mentions, almost in passing, that he and Alpöge believe they have blowup for hypo-dissipative Navier–Stokes, not yet Lean-verified, and that it is “suggestive of a path to unforced Euler.”[5] And on September 7, Anandkumar's group at Caltech posted evidence, from physics-informed neural networks refined to high precision, for a stable Euler singularity in free space without forcing, though their own manuscript says the stability constants are not yet certified.[16] Three groups, three methods, one target. If I had to bet on where the next month's real mathematics happens, it is here, not in the Clay fine print.

The month before the weekend

I have tried to keep the people out of the mathematics until now. That is no longer possible, because the timeline is itself part of what needs dissecting.

Here is what is not in dispute. Alpöge, a mathematician employed by Anthropic, and Buckmaster, at NYU, spent about a year on the Córdoba–Martínez-Zoroa program as what Buckmaster describes as “a purely personal collaboration,” paying for tools out of his own research funds. They used Claude, Codex with GPT-5.6 Sol, and later Astra for writeups and auditing. On August 15 they had Boussinesq and Euler blowup with smooth forcing. On August 22 the Lean verification finished. Buckmaster's description of the first machine-generated proof is “the most horrendous I have ever read,” and the weeks after were spent “around the clock” turning it into something a person could follow.[5]

Here is what OpenAI says. Bubeck, in the press call, said the company “began working on the Millennium problems due to viral twitter rumors that Anthropic had resolved 2 Millenium problems.”[17] Agents were launched on September 1. Roughly ten thousand of them ran concurrently for about 88 hours, exchanging about 2.7 million messages on Navier–Stokes and 4.9 million across all the problems attempted, producing about 130 billion output tokens. Formalisation took a further 17 hours using GPT-6 Astra; the proving model itself is described only as “significantly more capable” than that.[2][18] Cost, per Bubeck, “millions of dollars.” OpenAI's stated position on the pair's work is that “neither its researchers nor its agents saw any of the pair's work before it was released publicly,” that no one “searched through user data,” and, in the same breath, that it “cannot rule out that de-identified data derived from their usage of our products helped improve our models.”[17][19]

Here is what Buckmaster says happened in between, and I am going to quote rather than paraphrase, because paraphrase is how these things get distorted. On September 6, on calls that Alpöge did not join, Buckmaster was told an internal model had produced “about 100 pages” proving forced blowup, “option c and d in Fefferman.” He writes: “The route to the Clay problem through a smooth force ... is the route Luis and Diego opened and the one Levent and I had quietly chosen to attack. Almost nobody else I know of was working on it. ... When I heard ‘forced,’ it was a bright red flag.” He says he was shown a prompt and told the model “had simply been given the problem statement,” and that “very little human input” had been used, and that over the call “it emerged that an entire team had been working on the problem, that this was one of a number of things that was tried, that work had started on the unforced problem, that the team first set the model on easier problems, including Euler, that even the prompt that had been shown to me had been written by prompting Codex.” He describes two proposals: post Euler and let OpenAI post Navier–Stokes the next day, crediting the pair as the “closest humans to the problem”; or write up OpenAI's result himself, without Alpöge. He says he declined both, said he would go public, and was asked “Why would you ruin your career?” and later told “If you don't want me to be nice, then I don't have to be nice.” He closes: “I am not accusing anyone of anything. I am stating what I was told, when, and what was proposed to me.”[5]

Bubeck's response, on X and in the briefing, is that the allegations are “false and inflammatory,” that he “never ever asked for Levent to be removed from authorship of his own work,” that the discussion concerned whether Buckmaster might lead a rewrite of OpenAI's separate proof and whether an Anthropic employee authoring work produced by an OpenAI system would be appropriate, and that the career remark was “an ill-chosen remark made in frustration” which he retracted immediately.[20][21] Alpöge, per one account, declined repeated invitations to join the calls.[21]

I was not on the calls. Neither were you. What I can say is that both sides agree on the sequence: OpenAI started after rumours of the pair's progress reached it, chose the forced route the pair had been quietly working, and announced twelve hours after the pair's preprints. What they disagree about is why, and what was said in a room I cannot see. OpenAI has since said it “recognize[s] the priority of Levent Alpöge and Tristan Buckmaster's work,” and cedes the forced Euler result to them while claiming Navier–Stokes.[4][17]

Then there are the people whose names should have been the headline. Fefferman, who wrote the problem, told Quanta: “The heroes of the story ... are Córdoba and Martínez-Zoroa.” Córdoba: “Ten years ago, nobody believed there was a singularity for Navier–Stokes.” And, asked whether he uses AI: “I don't use AI: I have Luis.”[4] Buckmaster, in the middle of the worst week of his professional life, found room to write that “in view of this body of work, I believe Luis Martínez-Zoroa deserves a Fields Medal.”[5]

Tao's reaction is the one I keep rereading. On the mathematics: he blogged the Alpöge–Buckmaster results on September 7 as a breakthrough, said he saw no decisive obstacle to extending to Navier–Stokes, and wrote that “the primary goal of developing mathematical understanding and insight” outweighs “solving these problems” as a proxy.[3] On the week: “The indiscriminate strip-mining of open problems for solutions may destroy the ecosystem from which the next generation of mathematical techniques, problems, and practitioners would have developed,” like “using excavators to loot an archaeological site.” And the line that I think is the real result of September 2026: “There's been this very strange and unprecedented decoupling, this year alone, between getting answers and getting understanding.”[22][23]

The Clay Institute's president, Martin Bridson, said evaluation would be “deliberately unhurried” and “absolutely rigorous.” The problem is still listed as open.[23] OpenAI, for its part: “We do not intend to claim the Millennium Prize for this result.”[2]

Ten thousand agents, from someone who babysits five

I said at the top that my first reaction was a question about the prompt. Let me take that seriously for a paragraph, because it is my day job.

A hundred and thirty billion output tokens is roughly the token count of a large pretraining corpus, spent on one theorem. The announcement describes agents being “reallocated,” an internal model being “updated” mid-run, and “intermediate findings consolidated.”[18] That is an orchestration story, and the orchestration is the thing OpenAI has said the least about. We do not know the topology of the agent graph, how work was decomposed, how conflicting partial results were reconciled, how the 5 million messages were routed or summarised, or what the humans did between September 1 and September 5. Buckmaster's account of the call is the only description of the human layer that exists, and it says the team ran Euler first, tried the unforced problem, and wrote the prompt with Codex.[5] None of that is damning. All of it contradicts “very little human input,” and it is the kind of detail that decides whether this is a result about a model or a result about a lab.

I have watched five agents deadlock on a shared file. I do not have an intuition for ten thousand. Whatever the answer to the credit dispute, the system that produced 400,000 lines of kernel-checked Lean in 17 hours is a real artifact, and I would trade a lot of press releases for one honest engineering write-up of how it was built.

What this dissection does not say

It does not say the Millennium Prize problem, in the sense most people mean it, is solved. Alternatives (A) and (B) are open. Unforced breakdown, which is not one of the four alternatives, is open. Palasek's obstruction suggests the layered route does not extend to it without a new idea.[9]

It does not say the proof is wrong. I found no gap between the Formal Conjectures encoding and Fefferman's prose, the Lean proof is sorry-free under the three standard axioms, and the physical mechanism, once you write out the energy budget, closes. If someone finds a discrepancy, it will be in the 472 lines of encoding or in the toolchain, not in the 400,000 lines of proof.

It does not say the model did it alone. It does not say the model did it dishonestly. It says that a rumour started a race, that the race was run along a road two Spaniards had spent years paving and two other people had spent a year walking, and that the winner announced twelve hours after the runners-up, with a statement about training data that, by its own wording, cannot be checked from outside.

It does not say the 166 pages are readable. Buckmaster calls his own Euler write-up “AI slop” and apologises for it. I have read the OpenAI introduction and the proof outline closely, and they are clear and physically motivated. I have not read Section 9, and I do not know anyone who has yet.

And it does not say whose contribution the theorem “is.” The mechanism is Córdoba and Martínez-Zoroa's. The smooth-forcing rung is Alpöge and Buckmaster's for Euler. The viscous rung, the ripples, and the certificate are, on the available evidence, the machine's. Tao's word “decoupling” is the right one. We have a certified answer to a question that Fefferman wrote down in 2000, and the people who understand why it is true are still catching up to the fact that it is.

Reading order

On Monday I read Fefferman first, then the theorem, then the Lean statement, then the news. I recommend that order to anyone who wants to know what happened this week.

Read Fefferman and you learn that the problem has four doors, two of them let you push. Read the theorem and you learn the push is smooth, bounded, and switched off outside a box, and that a fluid at rest still reaches infinite speed under it. Read the Lean challenge and you learn exactly which door was opened, in a formalisation someone else wrote before the key existed. Then read the news and you learn that the door was opened at the end of a long corridor built by other people, some of whom were a few metres from the handle.

Option C was always in the document. The remarkable thing is not that somebody read it. It is that reading it carefully turned out to be worth several million dollars of compute, one Fields-Medal-worthy program from Madrid, a year of a personal collaboration, and a long weekend in September that none of us have finished dissecting.