Alpöge and Buckmaster prove AI-assisted finite-time blowup for 3D Euler
On 7 September 2026 Terence Tao described new work by Levent Alpöge and Tristan Buckmaster demonstrating finite-time blowup, with smooth forcing, for three fluid equations: the incompressible porous medium equation, the two-dimensional Boussinesq equation, and the three-dimensional incompressible Euler equations. The construction extends a method of Diego Córdoba and Luis Martínez-Zoroa, who had already settled the porous-medium case. The proofs were heavily AI-assisted — Alpöge is an Anthropic employee and the work used an internal Anthropic model — and were formalized in Lean. Buckmaster confirmed the result publicly late on 7 September, hours before OpenAI announced its own Navier–Stokes construction.
Why It Mattered
Taken on its own terms this is the more conventional of the week's two fluid-dynamics results, and for that reason arguably the more informative one about where AI-assisted mathematics actually stood in September 2026. It is human-led research at the frontier of a famously hard field, in which the machine contribution was substantial enough that the authors described their first draft as barely readable and spent weeks rewriting it into professional form. Tao's assessment is the relevant expert signal: the authors did not reach the Navier–Stokes goal, but made enough progress that completing it looked feasible in the near term — a judgement vindicated within a day. The episode documents a specific division of labour that became normal around this point: mathematicians choosing the strategy and stating the lemmas, models generating and repairing the technical construction, and autoformalization agents rendering the whole thing in Lean so that correctness no longer depends on a referee's patience. It also sets the factual baseline for the credit dispute that followed. Because the Euler result came first and OpenAI's agents were given an Euler result as a starting point, the question of who solved what, and on whose unpublished work, became concrete rather than rhetorical. The involvement of researchers linked to Anthropic on one side and OpenAI on the other turned an ordinary priority question into a proxy for competition between labs, and prompted the first serious public argument about whether using a commercial model on unpublished research leaks that research to its vendor. For the history of mathematics, the durable point is narrower and firmer than any of that: as of September 2026, machine-assisted arguments were producing genuinely new blowup constructions for classical PDEs, checked by machine.
Who Built It
Levent Alpöge and Tristan Buckmaster
Applications
- Mathematics
- Fluid Dynamics
- Formal Verification