PDE and mathematical physics · Sep 8, 2026
Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D
GitHub: openai/NavierStokesAndEuler, the Lean 4 formalizations
Contributors
GPT-6 Astra · Codex · OpenAI
AI systems: GPT-6 Astra, Codex
Sources
- GitHub: openai/NavierStokesAndEuler, the Lean 4 formalizations ↗
- OpenAI: Finite time blowup for Navier-Stokes (PDF) ↗
- Clay Mathematics Institute: the official problem description, alternatives (C) and (D) on page 2 ↗
- Formal Conjectures: the Lean statement of the Navier-Stokes problem the Comparator challenges adapt ↗
- OpenAI: On the Navier-Stokes Millennium Prize Problem ↗
- Clay Mathematics Institute: statement on the Navier-Stokes announcement ↗
- Terence Tao on the blowup results released the same week ↗