9 SEP 2026 — Tristan Buckmaster of NYU and Levent Alpöge of Anthropic have posted three preprints establishing finite-time blowup under smooth forcing for the incompressible porous medium equation, the two-dimensional Boussinesq system and the three-dimensional incompressible Euler equations. All three come with Lean formalisations in a public repository, which means anyone can check them by running a program.
What was proved, precisely
Finite-time blowup means a solution that starts smooth develops a singularity in finite time — some quantity becomes infinite. Whether that happens for fluid equations is one of the oldest open questions in analysis.
The results require a smooth forcing term — an external push applied to the fluid — and that is a real weakening. Constructing a blowup when you are allowed to design the push is a substantially easier problem than showing one arises from the fluid alone.
It is still substantial. Terence Tao, who has worked on this problem for years, called it a remarkable achievement, and the Euler result in three dimensions is the one that matters most.
The million-dollar framing is wrong
Coverage has reached for the Clay Millennium Prize, and the connection does not hold. That prize concerns existence and smoothness for the unforced three-dimensional Navier–Stokes equations. These papers are about Euler, and about forced systems.
Euler and Navier–Stokes differ by a viscosity term, and viscosity is precisely the mechanism that might prevent a singularity. A blowup for Euler is evidence about what the nonlinearity can do and is not a result about Navier–Stokes.
Forced versus unforced is the second gap. Once an outside force can be chosen freely, a great deal becomes constructible that the equations would not produce unaided. Both gaps are stated plainly by the authors; neither survives a headline.
Machine-checkable is the actual news
The formalisation is what separates this from an ordinary preprint. A Lean proof is checked by a program that verifies every inference against the axioms, so a reader does not have to trust the authors, the referees or their own reading.
That matters here more than usual, because the arguments were heavily AI-assisted. The authors describe their first write-up as the worst they had ever seen, and spent weeks turning it into something readable — a process that in an unformalised proof would be exactly where an error hides.
Formalisation removes that risk class entirely. Whatever a model contributed, the Lean checker does not care where a step came from, only whether it follows. This is the model of AI-assisted mathematics that works: generate freely, verify mechanically, publish the verification.
The dispute over the other claim
Alongside the papers, Buckmaster published an account of contact with OpenAI, in which he says the company told him an internal model had produced a roughly hundred-page proof of finite-time blowup for the forced Navier–Stokes equations. OpenAI announced its result on a call with reporters.
Set the two claims side by side. One team posted preprints and machine-checkable formalisations to a public repository. The other described a result to journalists. Those are not comparable acts, and only one of them can be evaluated by anyone outside the organisation making the claim.
A hundred-page unformalised proof is not nothing — most of mathematics looks like that — but it enters the world as a claim requiring months of referee time, and it was announced before that started. The credit dispute is downstream of the disclosure difference.
Why forced blowup is worth having anyway
The forced case tests whether the nonlinear structure of the equations can concentrate energy at all, and answering that constrains what a proof of the unforced case could look like.
It also has practical reach. Real fluids are forced — by gravity, by boundaries, by stirring — and a rigorous construction of a singularity under smooth forcing says something about what numerical simulations near such regimes are approximating.
The honest description is a significant result on a hard problem in a weakened setting, published in a form anyone can verify. That is a good week for mathematics and it is not a solved Millennium Prize.
What to watch
Whether the Lean formalisations survive scrutiny depends on whether they state the theorem people think they state, rather than on whether the proofs check. Formalisation guarantees the argument and not the definitions.
Whether OpenAI publishes anything checkable. And whether the technique extends toward the unforced case, which is the direction that would make this the beginning of something rather than a well-executed result about forced systems.
View author profile → · Editorial policy
