What happened?
Tristan Buckmaster and Levent Alpöge report finite-time blowup results with smooth forcing for the three-dimensional incompressible Euler equations, the planar inviscid Boussinesq equations and incompressible porous media, developed with substantial help from Claude and Codex; public Lean artifacts formalize the Euler and Boussinesq results.
The researchers explicitly credit Diego Córdoba and Luis Martínez-Zoroa for the underlying forced-blowup research program and describe using LLMs to push that program from rougher forcing toward smooth forcing and related fluid equations. The public `fluid_lean` repository contains complete Lean developments for the Euler and Boussinesq theorems, with its documentation attributing the Lean code to Claude under Alpöge's direction.
Why it matters
The event is an unusually inspectable example of AI contributing substantively to frontier mathematical research while humans retain the research program, judgment and responsibility for the claims. The results also became immediate historical context for the contemporaneous OpenAI Navier–Stokes claim, making precise attribution and separation of the distinct mathematical statements important to the Chronicle.
Significance rationale: The release combines three new smooth-forcing blowup results in major fluid equations with documented substantive LLM-assisted proof development and public Lean formalizations for the Euler and Boussinesq results. If accepted as H1, its historical significance comes from demonstrating human-led AI collaboration on frontier mathematical research, not from an AI originating the underlying research program.
Evidence & status at a glance
- Significance
- H1 · Historical milestone
- Verification
- Partially verified
- Evidence level
- E3 · Inspectable artifact
- AI role
- Human–AI collaboration
- Formal assurance
- Artifact available
How should these labels be read? →
Contribution & verification
- Mathematical novelty
- New result
- Interface
- Informal, Formal, Symbolic, Hybrid
- AI contribution
- Buckmaster's public account describes Claude and Codex as being used throughout the project with substantial help from LLMs in extending the existing program. The public Euler and Boussinesq Lean repositories state that all Lean code, including the trusted statement files, was written by Claude under Alpöge's direction. The authors explicitly state that the underlying research program was not originated by an LLM.
- Human contribution
- Buckmaster and Alpöge selected and developed the research direction, evaluated and organized the mathematical arguments, authored the released manuscripts and remained responsible for the claims. They credit Córdoba and Martínez-Zoroa with the foundational forced-blowup program; Alpöge directed and reviewed the public Lean formalization workflow.
- Verification
- Partially verified · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- claude, codex, lean, mathlib
- Organizations
- —
- Problems
- forced-euler-blowup, forced-boussinesq-blowup, forced-ipm-blowup
- Methods
- human-ai-collaboration, proof-development, formal-theorem-proving, lean
Verification history
- 2026-09-08 · Paper released · E3 · Inspectable artifact
Three manuscripts and a public Lean repository were released. The repository contains dedicated formalization projects for Euler and Boussinesq, while no corresponding IPM Lean project is present in the public repository tree.
- 2026-09-11 · Partially verified · E3 · Inspectable artifact
Terence Tao independently discussed the mathematical work and its relationship to the Córdoba–Martínez-Zoroa program, and OpenAI independently acknowledged Buckmaster and Alpöge's priority on the forced Euler result. These sources corroborate the event and its historical context but are not treated here as independent verification of all three underlying theorems or as an independent replay of the Lean artifacts.
Corrections
No corrections recorded.
