OpenAI Says Navier-Stokes Blows Up — And It Published the Lean Files

On September 8, OpenAI announced that an unreleased internal model had produced a proof on the Navier-Stokes existence and smoothness problem — one of the seven Clay Mathematics Institute Millennium Prize Problems, each carrying a $1 million award. The result: 3D Navier-Stokes can develop a singularity in finite time. The method: roughly 10,000 agents running for about 88 hours. The output: a 166-page paper plus public Lean proof files.

Within hours, the story stopped being about fluid dynamics and became about who gets credit for it.

The formalisation is the whole argument

Strip away the press-call framing and one detail carries the claim: OpenAI shipped machine-checkable Lean files alongside the paper.

That matters more than the page count. A natural-language proof of a Millennium Problem enters a review process measured in years — referees, counterexamples, a slow consensus that the argument holds. A Lean formalisation is a different object. It compiles or it does not. Anyone with the files and a proof assistant can check the logical chain themselves, and the only trust left to extend is trust in Lean's kernel and in whether the formal statement actually says what the English says it says.

That last gap is where mathematicians will spend their time, and they should. Formalising the wrong theorem is a real failure mode: a proof can be flawlessly machine-verified and still be a proof of something weaker, or differently quantified, than the headline. The interesting review over the next weeks is not "does it compile" but "is the Lean statement the Millennium Problem."

The initial reaction was blunter than that — mathematicians wanted to see files, not a press call. OpenAI then published the proof, which is the correct order of operations arriving one step late.

The claim is blow-up, not smoothness

Worth being precise, because the summaries have been sloppy. The Millennium Problem asks whether smooth, finite-energy initial conditions to the 3D incompressible Navier-Stokes equations always stay smooth, or whether solutions can break down in finite time. Both answers resolve it.

OpenAI's claimed result is the breakdown side: a singularity forms. That is the answer many working analysts have expected for years, and it is arguably the more tractable one, because constructing a blow-up scenario is a matter of exhibiting something rather than ruling everything out. Exhibiting it rigorously in three dimensions, with all the estimates closed, is still the thing nobody managed for ninety years.

The credit fight

Hours after the announcement, Tristan Buckmaster of NYU raised the possibility that OpenAI had drawn on his private research — work he and Levent Alpöge, now at Anthropic, had been developing for close to a year, some of it inside Codex sessions.

OpenAI's account: it completed its own proof and Lean verification on September 6, then contacted the two researchers to offer a joint announcement — and only at that point learned their work addressed a related but distinct problem, the forced Euler equations rather than Navier-Stokes. OpenAI researchers deny accessing private work or Codex logs. Buckmaster has separately alleged that OpenAI pressed him to leave Alpöge off any authorship.

Both accounts cannot be fully correct, and neither is currently verifiable from outside. What is verifiable is the structural problem underneath: a company that operates a coding assistant used by working researchers announced a result adjacent to a customer's unpublished research. Whether or not anything improper happened here, the arrangement guarantees this argument recurs. There is no clean way for a lab to prove a negative about its own log access.

The practical takeaway for anyone doing original work inside a vendor's agent: assume the boundary between your context window and the vendor's research organisation is a policy commitment, not a physical wall. Policy commitments are worth something. They are not worth what a local machine is worth.

Not claiming the money

OpenAI said it does not intend to claim the Clay prize. That is the right call and also the only available one — the Clay rules require publication in a refereed journal of international standing plus two years of general acceptance in the mathematical community. Nobody claims that prize in a week.

Declining it up front converts a potential embarrassment into a posture: we are not here for the million dollars, we are here to show you what the system did. Read cynically, it is also insurance. If the formalisation turns out to be a proof of a slightly different statement, "we never claimed the prize" is a much shorter walk back than a withdrawn submission.

What this actually measures

The number to sit with is not 166 pages. It is 10,000 agents for 88 hours.

That is a compute-shaped attack on a problem that has previously been attacked by individual mathematicians over decades. It says the frontier labs now believe research mathematics responds to parallel search plus formal verification — that you can throw a swarm at the space of proof strategies, let Lean act as the fitness function that kills every wrong branch immediately, and keep whatever survives.

Lean is the load-bearing part of that loop. Without a mechanical checker, 10,000 agents produce 10,000 plausible-looking arguments and no way to sort them. With one, the swarm becomes a search process with a hard oracle attached. That combination — cheap generation, exact verification — is the reason mathematics fell before most people expected it to, and the reason software engineering fell first.

The open question is what else has an oracle. Formal proof does. Compilers do. Circuit equivalence does. Protein structure sort of does. Most of the economy does not, and in those domains 10,000 agents mostly produce 10,000 confident opinions.

Navier-Stokes is not the story. The oracle is.