OpenAI vs Buckmaster: The Navier-Stokes Lean Proofs, Audited

On 8 September 2026, two groups published proofs that fluid equations can break down in finite time, and one accusation that the other group should not have got there.

Tristan Buckmaster of NYU's Courant Institute and Levent Alpöge, a mathematician employed by Anthropic, posted three papers and a Lean 4 formalization establishing finite-time blowup with smooth forcing for the incompressible porous media equation, for the planar Boussinesq system, and for the three-dimensional incompressible Euler equations. Roughly seven hours later OpenAI announced that an internal model had resolved the Navier–Stokes Millennium Prize problem, establishing alternatives (C) and (D) of the Clay Mathematics Institute's official formulation, along with an unforced Euler blowup.

Both announcements follow a week of rumour. OpenAI's own post says its effort began on 1 September after it heard that two Millennium problems had been resolved — the same rumour cycle that produced a viral prediction that Claude had solved Navier–Stokes. Buckmaster's statement, released the same morning, alleges that OpenAI began its effort only after learning about his and Alpöge's work, and describes calls in which he says he was pressured to reframe the credit. OpenAI's post says its researchers and agents "did not see any of their work" before publication.

Buckmaster's announcement on Mastodon, posted at 03:58 UTC, was three sentences and five links:

Today, Levent Alpöge and I have made public three results: finite-time blowup with smooth forcing for incompressible porous media, for Boussinesq, and for 3d incompressible Euler.

One half of this story is checkable today and the other is not. Both groups shipped machine-verifiable Lean certificates. Stanford Tech Review cloned and measured both.

What each side actually published

The four results in play are not the same result, and the distinctions carry the whole dispute.

Buckmaster and Alpöge proved blowup for forced Euler — a smooth external force is applied, and the fluid's vorticity becomes unbounded in finite time. OpenAI's Euler result is the unforced case, harder in the sense that the singularity must arise from the fluid's own motion. OpenAI's Navier–Stokes result reinstates viscosity and a smooth force, which is the route through Fefferman's options (C) and (D) rather than the celebrated (A)/(B) regularity question. OpenAI states plainly that it does not intend to claim the Millennium Prize for the result.

That route matters because it is the one Buckmaster says he and Alpöge had quietly chosen, following a program he credits to Diego Córdoba and Luis Martínez-Zoroa. He goes further than most authors would about the presentation: he calls his own Euler write-up, in his words, "AI slop," and apologises for it.

The three Buckmaster–Alpöge papers are a ladder rather than three separate results. Incompressible porous media is the most tractable of the three, Boussinesq is the classical two-dimensional model whose structure mirrors axisymmetric three-dimensional Euler, and the Euler paper is the one the field will read. Córdoba and Martínez-Zoroa had already obtained blowup with rough forcing along this route; the contribution Buckmaster claims for himself and Alpöge is pushing that to smooth forcing and to Euler, with heavy use of language models. He is unusually direct about where the credit belongs, writing that in view of that body of work he believes Martínez-Zoroa deserves a Fields Medal — a sentence that reads differently in a document otherwise concerned with credit being taken.

What Terence Tao said about it

The strongest independent read on the mathematics came from Terence Tao, who has worked on Navier–Stokes regularity for years and who posted his assessment within half an hour of Buckmaster's announcement. He calls it "a remarkable achievement," credits the underlying approach to Córdoba and Martínez-Zoroa exactly as Buckmaster does, and notes that Buckmaster had explained the key ideas to him by phone.

Two things in Tao's thread matter for the dispute. The first is his judgement, posted separately, that nothing in principle appears to prevent these methods from extending all the way to Navier–Stokes, with a non-negligible chance the forcing term could be removed entirely. Written before OpenAI's announcement, that is an independent statement that the road from Buckmaster and Alpöge's forced Euler result to the Millennium problem was visible to anyone who understood the method.

The second is that this was not a two-horse week. Tao also flagged a third, entirely independent result posted on 7 September by Ganeshram, Duruisseaux and Anandkumar at Caltech, which attacks unforced Euler blowup from the numerical direction using a physics-informed neural network. That work reports a promising and numerically stable candidate ansatz rather than a proof, and it is not part of the credit dispute. It is evidence that three separate groups converged on the same wall in the same week, which is the ordinary way hard problems fall and an awkward fact for anyone on either side arguing that only they could have got there.

The audit

We cloned both repositories on 8 September — tristanbuckmaster/fluid_lean and openai/NavierStokesAndEuler — and counted every .lean file, excluding vendored dependencies and Mathlib.

	Buckmaster–Alpöge	OpenAI
Lean files	3,612	2,484
Lines of Lean	1,684,580	616,274
Theorems + lemmas	68,179	35,731
Vendored lines	127,069	0
Unproven sorry	0	0
Placeholder sorry	3	4
Extra axiom	0	0
Lean toolchain	4.32.2	4.34.0-rc2
Prose pages	245	223
Repo created (UTC)	04:03:38	10:53:38
Commits	1	1

Line counts run by Stanford Tech Review on 8 September 2026. Method: all *.lean files per project, excluding vendor/ and .lake/.

The two certificates run to 2,300,854 lines of machine-generated Lean between them, against 468 pages of human-readable write-up. For Buckmaster and Alpöge that is roughly 6,900 lines of formal proof for every page of paper; for OpenAI, about 2,800. The largest single file in the Buckmaster–Alpöge tree, a time-estimates module named TimeRates.lean, is 101,042 lines on its own, and somewhere in that tree is a single line of Lean 47,419 characters long.

The important column is the one with the small numbers. A Lean formalization is worth exactly as much as its unproven holes and its extra axioms, and both projects come back clean: no axiom declarations at all, and every sorry sitting in a statement file where the comparator tooling requires a placeholder by design. Each project's README states that its proof rests on nothing beyond Lean's standard three axioms — propext, Classical.choice, Quot.sound. Anyone with a laptop and patience can check that claim; both repositories pin their Mathlib commit so the build is reproducible.

They pin different commits, on different toolchains, which means there is no shared build in which the two results can be checked against each other.

How to check it yourself

Neither claim requires taking anyone's word for it, which is the point of shipping a certificate. With elan installed, each project builds from its pinned toolchain and then reports the axioms its main theorem actually depends on:

cd fluid_lean/euler-blowup
lake build
lake env lean \
  scripts/PrintAxioms.lean

Buckmaster and Alpöge pin Lean 4.32.2, for which Mathlib publishes no prebuilt objects, so the dependency compiles from source and the build is long. OpenAI's repository targets 4.34.0-rc2 and can pull a cached Mathlib with lake exe cache get. In both cases the file a reader has to trust is the statement file — Challenge.lean on one side, the ComparatorChallenges directory on the other — because everything downstream of it is checked by Lean's kernel. Reading that one file carefully is the whole audit; the remaining two million lines are the machine's problem.

What the certificates cannot settle

Here is the limit of what we measured. A Lean certificate is a proof that a theorem follows from the axioms. It is silent on who found the argument, when, and with what help.

Both repositories were published as a single squashed commit, created six hours and fifty minutes apart on the same morning. Neither carries any development history. Every date in this dispute — Buckmaster's 15 August for the blowup results and 22 August for the Lean verification, OpenAI's 1 September launch and 5 September resolution — rests on testimony, not on version control. That is unremarkable practice for a research artifact, and it is also the reason the provenance argument cannot be resolved by anyone outside the two groups.

OpenAI's account is specific about scale: around 10,000 concurrent agents on the Navier–Stokes group, 2.7 million messages and roughly 130 billion output tokens for that problem alone, with Lean verification taking a further 17 hours. Buckmaster's account of the 6 September calls is equally specific and considerably less flattering, including his recollection that when he said he would go public he was asked, "Why would you ruin your career?"

Sébastien Bubeck, the OpenAI scientist Buckmaster names, has since responded on X. He does not address the allegations individually, says he entered the discussion following academic norms, and promises a fuller account:

A series of false and inflammatory allegations against me are currently circulating on social channels. To clarify, I came into the discussion following academic norms, and I'm disappointed that it has come to this. Anyone who knows me knows that academic standards are of the highest importance to me. Will have more to say tomorrow.

— Sebastien Bubeck (@SebastienBubeck) September 8, 2026

So the two accounts of those calls are now formally in conflict, with the detailed version on the record and the denial still to be filled in. We have not seen anything that would let us adjudicate between them, and we are not attempting to. Buckmaster is careful on this point himself: he says he has not seen OpenAI's proof and is not accusing anyone of anything.

What mathematicians said in the replies

The reaction under Buckmaster's Mastodon post converged on two readings, neither of them the one the headlines took.

The first is technical, and it reframes the data question. Talia Ringer, a programming-languages researcher who works on machine-assisted proof, replied that the relevant mechanism is not lookup but reinforcement learning on a corpus of chats gathered from users who did not opt out — and that the open questions are when the last training run happened and whether a model would memorise so small a fragment. That is a narrower and more testable claim than "they read our drafts," and it is compatible with OpenAI's own wording, which denies accessing specific user data while conceding it cannot rule out that de-identified derived data helped improve its models.

The second reading, posted by the Mathlib maintainer Joseph Myers and carried over from the Lean community's Zulip, sets provenance aside entirely. It asks whether a company that both supplies the tools researchers use and competes against those researchers can avoid the appearance of a conflict of interest, whatever actually happened. On that framing the interesting question is structural, and no audit of anyone's Lean code will answer it.

A third, more sceptical strand pushed back on Buckmaster: one reply argued that if the "help improve the model" setting was left at its default, no terms were broken. Buckmaster's own follow-up sharpened his objection to a date rather than a permission, noting that OpenAI says it has been training the model since 28 August — after his results were obtained.

The part everyone agrees on

Buckmaster's statement says the results are not the important thing, and he is right, though not for the reason the dispute suggests. In his telling, the first machine-generated proof his collaborator sent him was the worst he had ever read, and it verified in Lean seven days later. He calls this a Deep Blue–Kasparov moment and says the community needs an unhurried discussion about credit, refereeing, and training.

Tao got there three days early. On 5 September, responding to the rumours before anyone had published anything, he warned about the opportunity cost of converting a historically productive problem into a viral post advertising benchmark progress, rather than advancing the field.

That discussion is going to be harder than the mathematics, and the certificates published today are evidence for it either way. Two million lines of verified Lean settle the theorems completely and settle nothing about the people. For 90 years the bottleneck on this problem was finding an argument. As of this morning the bottleneck is agreeing on who found it.

Cover image: von Kármán vortex street off the Cape Verde Islands, GOES-16 imagery, CSU/CIRA and NOAA, public domain.