On 8 September, OpenAI said an internal model had proved that the Navier–Stokes equations can develop a singularity in finite time, and published both a written proof and a formalisation in Lean. Within a day the story circulating was a different one: that the company had read a mathematician’s private conversations to get there.
Nobody alleges that. Not the press, not OpenAI’s critics, and not the mathematician.
Tristan Buckmaster’s actual complaint is narrower, better evidenced, and more interesting. And the technical objection most coverage raised against the proof — that its forcing term disqualifies it from the prize — is wrong, which anyone can confirm in about four minutes by reading the official problem statement instead of the reporting about it.
The accusation nobody made
The viral version has OpenAI reaching into private Codex sessions and lifting a proof. What Buckmaster says is that “information about our progress had been passed to OpenAI”, and that the route the company then took was too specific to be coincidence: “it is not the direction one arrives at in a few days by giving a model the problem statement.”
He did separately ask whether the model had been trained on, or had access to, the Codex sessions where he and Levent Alpöge kept their drafts. He reports being told the model did not look up user data. On the training question, he writes, “I did not get an answer.”
That gap is real and worth pressing on. It is not surveillance, and calling it surveillance buries the allegation OpenAI has actually had to answer.
OpenAI’s denial is precise about access and hedged about training, and the two halves are worth reading as a pair:
We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem.
While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models.
Firm on the first, soft on the second — which is exactly where Buckmaster says he got no answer.
The forcing term is allowed, and the coverage said otherwise
This is the part worth the reader’s time, because it is checkable and most reporting got it backwards.
OpenAI’s proof produces a blow-up in a fluid that has a smooth external force applied to it. Several outlets treated that as fatal, reporting that the Millennium Prize formulation requires the unforced case. The Clay problem is defined by Charles Fefferman in a six-page document, and it asks for a proof of one of four statements. Two of them require the force to vanish. Two of them do not:
(C) Breakdown of Navier–Stokes solutions on R³. Take ν greater than 0 and n = 3. Then 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 (p, u) of (1), (2), (3), (6), (7) on R³ × [0,∞).
The bolded clause is the whole argument. A forcing term is not a loophole in statement C; it is written into it. Statements A and B are the ones that fix the force at zero, and they are the existence-and-smoothness statements — the other side of the question entirely.
OpenAI claims exactly this, and says so plainly: the result “resolves the Navier–Stokes Millennium Prize problem by establishing statement ‘C’ (and also ‘D’)”.
So the live objection is not that forcing was used. It is narrower, and nobody has published an answer to it: whether the particular force in this proof satisfies conditions (4) and (5), which demand smoothness and rapid decay in space and time, and whether the Lean statement is logically equivalent to C.
What the announcement actually says about scale
The compute figures circulated in a mangled form, mostly because a total was reported as a subtotal. OpenAI’s own document splits them.
| Figure | Commonly reported | In the announcement |
|---|---|---|
| Inter-agent messages | ~5 million, for Navier–Stokes | 2.7 million for Navier–Stokes; 4.9 million across every problem attempted |
| Output tokens | not reported | ~130 billion for Navier–Stokes; ~300 billion in total |
| Concurrent agents | thousands | on the order of 10,000, in the group that found it |
| Time to a proof | 88 hours | 88 hours, from launch on 1 September to resolution on 5 September |
| Formalisation | 17 hours | 17 further hours, in Lean, run by GPT‑6 Astra — not the model that found the proof |
| Compute cost | “several million dollars” | not stated; that is an estimate given to reporters, not a published figure |
Two details in that table do more work than the headline numbers. The proof was found by an internal model still in training, begun on 28 August and described as substantially more capable than the company’s shipping model — so the result is not a demonstration of anything the public can use. And the formalisation was done by a different, weaker model, which is a reasonable division of labour and also means the Lean output was produced by a system nobody is claiming solved the problem.
There is one more figure that changes how the dispute reads. OpenAI’s agents also resolved the Euler blow-up question — the same problem with viscosity removed — using roughly 100 agents over about 50 hours, and they resolved the unforced version. Buckmaster and Alpöge proved the forced case. On Euler, the two results are not the same theorem, and OpenAI’s is the stronger one. That distinction is the company’s actual defence of independence, and it went missing from almost every summary.
Two accounts of the same week
Where the accounts agree, they agree on dates. Where they diverge, they diverge on two specific days.
| Date | OpenAI’s account | Buckmaster’s account |
|---|---|---|
| 15 Aug | — | Work with Alpöge on finite-time blow-up for forced 3D Euler, extending Córdoba and Martínez-Zoroa |
| 28 Aug | Begins training the internal model later used for the proof | — |
| 1 Sep | Hears a rumour that two Millennium problems have fallen; launches an effort, prompting separate agent groups with variants A, B, C and D | — |
| 3 Sep | Not mentioned | Emails an OpenAI mathematician to clarify the work is a personal collaboration |
| 5 Sep | Agents reach the Navier–Stokes resolution, 88 hours after launch | — |
| 6 Sep | Lean verification completes; reaches out to offer a concurrent release and “to recognize their priority in a joint announcement” | Two calls. Says he was offered the prize claim on condition he credit OpenAI’s solution and remove his co-author’s name; quotes “Why would you ruin your career?” and “If you don’t want me to be nice, then I don’t have to be nice.” |
| 7 Sep | — | Terence Tao posts on the Alpöge–Buckmaster results, noting the work is “heavily AI-assisted” |
| 8 Sep | Announces the result, the writeup and the Lean certificates | Posts three preprints and a public statement |
The 3 September row matters because OpenAI’s announcement presents the contact as something it initiated on 6 September, after finishing. Buckmaster has him writing to an OpenAI mathematician three days earlier, before any proof existed. Both cannot be the first contact.
The 6 September row matters more. OpenAI describes an offer of joint credit. Buckmaster describes an offer conditional on removing a co-author — Alpöge is employed by a competitor — alongside two remarks he quotes directly. OpenAI’s written announcement neither mentions this nor denies it.
The company’s own framing concedes more than the summaries noticed:
Our effort began on September 1st after hearing a rumor which we later realized was related to Levent Alpöge… and Tristan Buckmaster.
The causal chain Buckmaster alleges is therefore not in dispute. What is in dispute is what the rumour carried. OpenAI’s position is that it conveyed only that problems had fallen, which is why agents were prompted with all four variants rather than aimed at C. Sébastien Bubeck separately told reporters that the Navier–Stokes approach “did follow a similar method” to the pair’s — a concession that appears nowhere in the written announcement.
What is established, and what is not
Established. OpenAI published a written proof and a Lean formalisation on 8 September, with the certificates public under an Apache-2.0 licence and a pinned toolchain, so the formal artefact can be rebuilt by anyone. The company states it does not intend to claim the prize. Fefferman’s statements C and D permit a smooth forcing term. The Clay Mathematics Institute still lists the problem as unsolved, and its rules require a qualifying publication, two years in public and general acceptance before it will consider a claim. OpenAI’s Euler result is the unforced case; the Alpöge–Buckmaster Euler result is the forced case.
Claimed, and consistent with what has been published. That the proof establishes statement C. That the effort was independent of the pair’s work. That no specific user data was accessed.
Not established. Whether the force constructed in the proof satisfies conditions (4) and (5). Whether the Lean statement is logically equivalent to Fefferman’s C — a check a machine cannot do for you, because the machine only confirms that the proof follows from whatever statement it was handed. Whether de-identified training data derived from the pair’s usage contributed anything. What was said on the calls of 6 September. And whether the mathematical community accepts the result, which is the only test that eventually counts.
What a reader should take from this
A machine-checked proof is a conditional guarantee, not an absolute one. Lean verifies that a proof follows from a statement. It has nothing to say about whether the statement is the one you meant. Quanta put the remaining human task precisely: guaranteeing that what was shown true in Lean is logically equivalent to what mathematicians set out to prove. That gap is where every formal verification effort lives, and it is not a criticism of the tool.
“Solved” and “eligible” are different words. The proof may be entirely correct and still take years to be accepted, because acceptance is a social process with a published waiting period attached to it.
Verification is available here in a way it usually is not. The artefacts are public and buildable. Anyone with Lean and the patience to read a formal statement can settle the central open question without anyone’s permission, which is a genuinely unusual position for a disputed result to be in.
Attribution gets harder from here, and the interesting version is not theft. Both sides of this dispute used AI assistance heavily — Tao notes the Alpöge–Buckmaster proof is “heavily AI-assisted” — so the clean human-versus-machine framing does not survive contact with either party. The question that outlasts this story is not who copied whom. It is what credit means when the unpublished part of research increasingly happens inside someone else’s infrastructure. This site takes a narrow position on the adjacent question of disclosure, which is set out with the rest of how a page here gets made.
Nothing above is a judgement on whether the proof is correct. It is an account of which claims are sourced, which are contested, and which one is sitting in a public repository waiting for somebody to check it.
Sources
Two primary documents were read in full: OpenAI’s announcement and Fefferman’s official problem statement, from which statement C above is quoted directly. Everything attributed to Buckmaster is his own public account, and is marked as such where it appears.
- OpenAI — On the Navier–Stokes Millennium Prize Problem — the announcement, the compute figures and the statement-C claim
- Charles L. Fefferman — Existence and Smoothness of the Navier–Stokes Equation — the official Clay problem, and the source of statements A through D
- openai/NavierStokesAndEuler — the Lean certificates, Apache-2.0, with a pinned toolchain
- Terence Tao — Finite time blowup with smooth forcing term — on the Alpöge–Buckmaster results
- TechCrunch — OpenAI fought dirty on a career-making math problem, says NYU mathematician — the conduct allegations
- Scientific American — OpenAI claims blockbuster math breakthrough amid swirl of controversy
- Quanta Magazine — AI has solved one of maths’ $1 million Millennium Prize problems — the outstanding human verification step
- Unite.AI — Buckmaster and Alpöge post proofs, dispute OpenAI contact — the 3 September email and the call timeline