Contents
On September 7, NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge posted three preprints, each with a Lean formalization attached, proving that the incompressible porous medium equation, the two-dimensional Boussinesq system, and the three-dimensional incompressible Euler equations can all develop singularities in finite time under smooth forcing. A day later Buckmaster posted a statement describing calls with OpenAI in which, he says, he was told an internal model had produced a roughly hundred page proof of blowup for the forced Navier-Stokes equations, one of the Clay Institute’s Millennium Prize problems, and was asked to either drop his coauthor from the paper or credit the model as the one that closed the gap. That combination, a real formally-verified mathematical result plus a fight over who gets to say they solved what, is worth more attention than either half on its own.
The mathematics matters independent of the dispute. Finite-time blowup for Navier-Stokes, whether a smooth solution can develop a singularity in finite time, has been open since the Millennium Prize problems were named in 2000. Nobody has resolved the unforced case. What Buckmaster and Alpöge did is extend a program started by Diego Cordoba and Luis Martinez-Zoroa, which showed blowup was reachable when you’re allowed to add a smooth external forcing term, to Euler and Boussinesq, and they backed every claim with a Lean certificate rather than asking anyone to trust a hundred pages of estimates.
How the construction actually works
The core idea is an iterated correction, not a single clever solution. Start with a low-frequency background solution to the forced equation. At each stage, add a high-frequency correction to the solution that grows in amplitude as you approach a target blowup time, while the corresponding correction to the forcing term stays small. Terence Tao, writing about the papers, described the trick as timing the emergence of large amplitudes so that by the blowup time the solution has become singular without the forcing term ever losing its smoothness. Do this once and you have a perturbation. Do it as an infinite tower of corrections at successively higher frequencies, with the time cost of each stage shrinking fast enough that the whole tower fits inside a finite time window, and you have blowup.
The AI’s role here was writing, not discovering. The papers’ own disclosures say Claude and Codex handled the bulk of the write-up, including bookkeeping for the inductive constants that make these estimates so tedious to check by hand, while the authors supplied the mathematical direction. Buckmaster is blunt that the first machine-generated draft was close to unreadable, and that the released Euler paper is still closer to model output under human supervision than to a paper a mathematician would write unaided. The Lean formalization is what makes that acceptable: you don’t have to trust the prose, you can run the checker.
None of this touches unforced Navier-Stokes. The forcing term is doing real work in all three proofs, and removing it is exactly the hard, unsolved direction of the actual Millennium Prize problem. Whatever OpenAI’s internal model produced, if it produced anything, Buckmaster says he has not seen it and does not know whether it used forcing, whether it has been Lean-checked, or whether it exists in a form anyone outside OpenAI can verify.
Try it: why the tower converges in finite time
About this model
This is a simplified illustration of the iterated-correction mechanism Tao describes, not a reconstruction of the actual proof or its constants.Move the sliders to run the tower.
Push frequency growth well above amplitude growth and the forcing term collapses toward zero while the solution still diverges, that’s the regime the real papers live in. Push amplitude growth past frequency growth and the forcing term explodes right alongside the solution, which is the failure mode the actual estimates spend hundreds of pages ruling out.
What I’d take from this
Set the OpenAI dispute aside for a moment and the underlying trend is the one worth tracking: AI-assisted proof writing paired with machine checking is turning “trust me, I checked the algebra” into “here’s the Lean file, check it yourself.” That’s a genuinely good direction, and it’s the same pattern behind Claude’s Fermat’s Last Theorem formalization I wrote about a few days ago. The dispute is worth tracking too, but for a different reason. If frontier labs are racing to be first to announce results built on researchers’ own draft work, the incentive to verify claims independently, rather than take an announcement at face value, only gets stronger. My next move is watching whether OpenAI publishes an actual Lean-checked Navier-Stokes proof or a press release, because right now the record is one of those and not the other.