Tao Hails AI-Assisted Fluid Blowup Breakthrough, Formalized in Lean
Terence Tao blogged about a new breakthrough by Levent Alpöge and Tristan Buckmaster on fluid equation regularity, calling it "a remarkable achievement," noting substantial AI input in the argument and that the work has been formalized in the Lean proof assistant. The direction relates to one of the Millennium Prize Problems—global regularity of the 3D incompressible Navier-Stokes equations, worth $1 million.
Confirmed
- Building on work by Córdoba and Martínez-Zoroa, Alpöge and Buckmaster proved finite-time blowup for three simpler model equations: the incompressible porous medium equation, the 2D Boussinesq equations, and the 3D incompressible Euler equations (per @peterjliu and @MannyKayy relaying Tao's blog).
- Tao called the result "a remarkable achievement" with substantial AI input, and the authors have been advancing rapidly in this direction (@Hesamation).
- The argument has been formalized in Lean (@peterjliu, @MannyKayy).
- @basedjensen summarized that the field is moving "unusually fast": beyond the smooth-forced Euler result, another team independently produced related unforced results, and Tao believes a full smooth-solution proof may now be feasible.
- @alexisgallagher relayed that the community now broadly expects blowup solutions to be constructible under relevant smooth initial conditions, moving closer to the full Navier-Stokes problem.
- Several posts (@burnytech, @LucaAmb, @Singularitarian) note Tao believes the blowup mechanism may extend to Navier-Stokes itself; @Singularitarian also mentioned an OpenAI connection, without details.
Unconfirmed
- A full blowup/regularity result for the 3D incompressible Navier-Stokes equations remains unproven; current conclusions cover only model equations and the smooth-forced case.
- The OpenAI connection mentioned by @Singularitarian lacks detail and cannot be verified.
Why it matters
- The progress follows the strategy of proving blowup first on simpler model equations before approaching full Navier-Stokes, a substantive advance on a Millennium Prize problem.
- Deep AI participation (explicitly highlighted by Tao) plus Lean formalization demonstrates a new paradigm of human-AI collaboration in frontier mathematics.
2026-09-08 ~ 2026-09-10 · 9 related posts
Primary sources
- Terence Tao hails AI-assisted math breakthrough, says methods could extend to Navier-Stokes — Hesamation ·
- Tao Flags Major Break Toward Navier-Stokes Blowup, Formalized in Lean via Autoformalization Agents — peterjliu ·
- Tao says Navier-Stokes blowup proof is close: AI-assisted work formalized in Lean — littmath ·
- [source] Tao Flags Major Break Toward Navier-Stokes Blowup, Formalized in Lean via Autoformalization Agents — peterjliu · 2026-09-08
- Fluid Regularity Landscape Moving Fast: Tao Says Smooth NS Now Looks Feasible — basedjensen · 2026-09-08
- Terence Tao blogs on Buckmaster and Alpöge's blow-up solutions to fluid equations — LucaAmb · 2026-09-08
- [source] Terence Tao hails AI-assisted math breakthrough, says methods could extend to Navier-Stokes — Hesamation · 2026-09-08
- Alpöge and Buckmaster release smooth-forced blowup results; Tao says machinery may extend to Navier-Stokes — burny_tech · 2026-09-08
4 near-duplicate retellings: Singularitarian · MannyKayy · littmath · alexisgallagher