What was actually proved
Levent Alpöge and Tristan Buckmaster have posted three preprints establishing finite-time blowup with a smooth forcing term for the incompressible porous medium equation, the two-dimensional Boussinesq system, and the three-dimensional incompressible Euler equations.
Terence Tao wrote about the results on Monday, noting that the arguments are “heavily AI-assisted” and that the work has also been formalised in Lean. He credits the underlying programme to Diego Córdoba and Luis Martínez-Zoroa, who handled the porous medium case first.
Blowup means the equations produce a solution whose speed becomes infinite in finite time — a mathematical breakdown, not a physical one. Establishing it for Euler with forcing is a step on the road to the same question for Navier-Stokes, which carries a Clay Millennium Prize.
The AI part
Buckmaster is at NYU. Alpöge is a researcher at Anthropic. According to Unite.AI, the pair disclosed using Anthropic’s Claude and OpenAI’s Codex for bookkeeping of inductive orders and constants, and for iterative refinement of the writeup.
They were blunt about the quality of what the models produced in prose. Buckmaster described the initial AI-generated text as “the most horrendous I have ever read”, and the authors called their first draft the worst writeup they had ever seen. The Lean formalisation is the part that carries the certainty: a proof assistant either accepts an argument or it does not.
The dispute
In a statement published alongside the preprints, Buckmaster says OpenAI told him an internal model had produced a roughly 100-page proof of finite-time blowup for the forced Navier-Stokes equations. He describes two conversations on 6 September involving OpenAI researchers, among them Sébastien Bubeck.
Buckmaster says OpenAI proposed either that the two groups publish on consecutive days, with OpenAI’s Navier-Stokes result following his Euler paper, or that he write up the Navier-Stokes result alone, crediting an unnamed internal OpenAI model, with Alpöge dropped from the authorship — a point Buckmaster connects to Alpöge’s employment at Anthropic. He reports being asked why he would ruin his career after declining. He also says he asked whether his team’s Codex sessions had been used in training and, in his words, did not get an answer.
Buckmaster is careful in the statement: he has not seen OpenAI’s proof, and he writes that he is not accusing anyone of anything.
Bubeck has rejected the account. OfficeChai reported that he called the claims false and inflammatory, said OpenAI did not use the pair’s prompts or proofs to prompt its own models, and said he had entered the discussion following academic norms. He said OpenAI reached Euler independently by different methods, and that its Navier-Stokes work used a similar approach, developed over a weekend.
What is and is not settled
The Alpöge–Buckmaster results are public and Lean-verified. OpenAI’s Navier-Stokes claim is not: as of Monday the company had not posted the result to its own news page, and no third party has inspected the proof.
Even if it holds, the Millennium Prize question is not obviously answered. Scientific American reported Buckmaster’s own caveat that some in the community may say the problem has not really been solved, because the forced version relies on a term the classical formulation excludes.
What to watch is narrow and checkable: whether OpenAI releases the proof and its Lean certificate for others to verify, and whether the Clay Mathematics Institute says anything about forcing terms. Until the first happens, one side of this story has published its work and the other has described it.
