OpenAI Solved Navier-Stokes. Read the Compute Bill

On 8 September OpenAI announced that an internal model had produced a proof that the three-dimensional Navier–Stokes equations can develop a singularity in finite time — a question open for roughly ninety years and one of the seven Millennium Prize Problems.

It is a genuinely significant result. It is also being reported in a way that gets several things wrong, and the most interesting part of it has almost nothing to do with mathematics.

• ▸It was not ChatGPT. OpenAI used an unreleased internal model it describes as significantly more capable than GPT-6 Astra. It is not a product, and you cannot use it.
• ▸It does not claim the prize. OpenAI is not claiming the $1 million Millennium Prize, and the Clay Mathematics Institute has not commented on the result.
• ▸The AI did not do it alone. Charles Fefferman of Princeton, who wrote the official description of the problem, put it plainly: the heroes of the story are Córdoba and Martínez-Zoroa — the mathematicians whose technique of infinite cascades of non-singular solutions the proof builds on.

What was actually proved is that a singularity forms, under smooth forcing. That settles the question in the negative direction: smooth fluid motion can break down. It is not a proof that the equations behave well, which is what most people assume 'solving Navier–Stokes' means.

OpenAI's own figures for the run:

• ▸Roughly 10,000 concurrent agents.
• ▸2.7 million messages between them, and approximately 130 billion output tokens.
• ▸88 hours from launch to result, reached on Saturday 5 September.
• ▸A 165-page proof at the end of it.
• ▸A further 17 hours for GPT-6 Astra to formalise and verify that proof in Lean.

The cost is genuinely unsettled. Fortune reports a range of $2 million to $22.5 million. Simon Willison worked out roughly $15 million at public API pricing for the 300 billion output tokens spent across all the problems attempted. CNBC has cited $10 million. Nobody outside OpenAI knows, and internal compute does not cost what the API charges.

Set the mathematics aside for a moment and look at the shape of the run.

The search — 10,000 agents, 88 hours, millions of dollars — produced a candidate. The verification took 17 hours and produced certainty. One of those halves is expensive and unrepeatable; the other is cheap, mechanical, and something anybody with a Lean installation can rerun.

It is also why this worked on mathematics and has not worked on most things. Very few domains have a Lean — a way to mechanically verify that a proposed answer is correct, independently of how much you trust whatever produced it.

Directly, nothing. No amount of local hardware is in this conversation; the gap between a desktop graphics card and 10,000 concurrent agents is not one you close with a better GPU.

Structurally, quite a lot, because the asymmetry above is the same one that decides where a small local model earns its keep.

• ▸Tasks where you can cheaply check the output are the ones to give a smaller model. Code that either compiles and passes tests or does not; extraction you can validate against a schema; classification you can spot-check. A weaker model plus a cheap verifier often beats a stronger model you have to trust.
• ▸Tasks where checking is as hard as doing are where model quality actually matters, and where local models genuinely struggle. Summarising a document you have not read, or advice you cannot evaluate, gives you nothing to check against.
• ▸Sampling several times and verifying is a strategy, not a hack. It is a scaled-down version of exactly what OpenAI did here, and it is available on one GPU.
• ▸This is why coding agents work better than they should. The test suite is the verifier.

Twelve hours before OpenAI's announcement, Tristan Buckmaster of NYU and Levent Alpöge of Anthropic announced that they had resolved several closely related problems on the Euler equations, with help from a range of AI models.

Buckmaster has since raised serious concerns. He questions whether OpenAI's model had access to, or was trained on, his sessions in Codex, and says he did not get clear answers. He further alleges that OpenAI's Sébastien Bubeck proposed he could publish and claim the prize provided he acknowledged OpenAI's solution and removed Alpöge's name because of his Anthropic affiliation, and that Bubeck made remarks he took as threats to his career.

Bubeck denies the substance: OpenAI did not use their prompts or proofs to prompt its models or direct its agents, and has since said it has nothing but congratulations for their work. OpenAI does concede one thing worth reading carefully — that it cannot rule out that de-identified data derived from their use of its products helped improve its models.

These are allegations and denials, not established facts, and they are unresolved. They are also the part of this story most likely to matter in a year, because they are about what happens when the tool a researcher works in is owned by a competitor for the same result.

Tao's criticism is not that the result is wrong. It is that AI companies are treating open problems as marketing, and that an autonomous answer yields far less than a human route to the same place — the techniques developed along the way are usually worth more than the theorem.

He compared the strip-mining of open problems to archaeological looting: you get the object and destroy the context that would have told you what it meant. Whether or not you agree, it is the most substantive objection anyone has raised, and it is not answered by the proof being correct.

• ▸A real result, from an internal model nobody outside OpenAI can use.
• ▸It proves blow-up under forcing, not that the equations are well-behaved. No prize is being claimed.
• ▸Two human mathematicians developed the technique it rests on, and the person who wrote the problem statement says they are the story.
• ▸Search cost somewhere between $2M and $22.5M. Verification cost 17 hours — and the verification is why the search was worth funding.
• ▸The credit dispute and Tao's objection are both unresolved and both matter.

If there is one thing to take from it, it is not that models got smarter. It is that expensive search plus cheap verification beats trusting any single answer — which is as true on one GPU as it is on ten thousand agents.