Sep 8, 2026
Smooth compactly supported unforced Euler blowup
Model / AI: OpenAI (unreleased), GPT-6 Astra
machine-checkedself-reported
OpenAI reports that nearly 100 agents worked for about 50 hours to construct smooth, compactly supported, divergence-free initial velocity whose unforced three-dimensional Euler solution has finite maximal lifespan, unbounded velocity-gradient norm and divergent time-integrated vorticity norm. The released 57-page paper gives the analytical construction, and the shared Lean repository reports two zero-sorry formulations using only Lean's three standard axioms.
Source read 2026-09-08. Read the announcement, paper abstract and Theorem 1.1, and the repository's scope and formalization metadata. The full proof was not audited and the Lean development was not rebuilt.