Finite-time blowup for the unforced Euler equations from smooth compactly supported data
A Lean development proves that the three-dimensional incompressible Euler equations, with no forcing term, develop a singularity in finite time from smooth, compactly supported, divergence-free initial velocity on all of space.
- Lab
- OpenAI
- Model
- Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization
- Field
- Mathematics
- Date
- 2026-09-08
Sources
Original work
Announcement
Media coverage
Independent commentary
What was found
Whether the three-dimensional incompressible Euler equations can produce a singularity in finite time from smooth finite-energy data, with no forcing and no boundary, is one of the long-standing questions in mathematical fluid dynamics. The repository states the result twice: euler_breakdown_R3, that no global smooth unforced solution of uniformly bounded kinetic energy exists on R^3, and exists_compact_smooth_euler_singularity, which gives compactly supported smooth initial data with a positive finite maximal lifespan in the all-order Sobolev class, an unbounded limsup of the velocity's C^1 norm, and a divergent time integral of the vorticity's sup norm. That last condition is the Beale-Kato-Majda quantity, so the blowup is certified in the classical criterion rather than only as a loss of regularity. Both theorems are recorded with no sorry and dependence on exactly propext, Classical.choice and Quot.sound, and the Comparator config enables the independent nanoda kernel. OpenAI's account describes roughly 100 agents working about 50 hours on this result, against roughly 10,000 over 88 hours for the companion Navier-Stokes work. Euler is not one of the Clay Millennium problems; that list carries Navier-Stokes only.
Novelty check
The gap this closes is specific and the prior literature marks it clearly. Elgindi proved finite-time singularity for axisymmetric no-swirl Euler on R^3 at C^{1,alpha} regularity, and Elgindi and Pasqualotto did the analogous thing for Boussinesq, in both cases below smooth. Chen and Hou proved blowup for smooth finite-energy data by computer-assisted analysis, but in an axially periodic cylinder with an impermeable wall, so with a boundary (PNAS, 2025). What remained open was exactly the case claimed here: smooth, compactly supported data on R^3 with no boundary and no forcing. No prior claim on that case was found in the four registries or in the search behind this note. The companion result released the same week by Alpoge and Buckmaster is finite-time blowup for Euler with smooth forcing, which is a weaker and different statement, and the two should not be read as competing claims on the same theorem.
Caveats and known objections
Verification is graded claimed rather than formal despite two theorems with no sorry and exactly the three standard axioms. The repository's own formalization.yaml records its review status as self-assessed, and no mathematician outside OpenAI is on record as having read the argument at entry. Statement fidelity carries more weight on this entry than on the companion Navier-Stokes one, and the difference is worth stating plainly: there, the Comparator reference statements were adapted from Google DeepMind's Formal Conjectures formalization of the Clay problem, so the statement being proved against had independent provenance. The repository records no such outside source for the Euler challenge module, so what the kernel compares against is the repository's own formalization of its own theorem, and a reader checking this should start by reading ComparatorChallenges/Euler.lean against the paper rather than by rerunning the build. The model attribution is split and both halves are recorded above: the announcement describes an unnamed next-generation model, while the repository metadata credits GPT-6 Astra through Codex under an agent method, which most plausibly describes who wrote the Lean rather than who found the proof. Autonomy is ai-led rather than autonomous because the disclosure describes an agent framework without stating the run was unsteered. The priority dispute around the same week's releases is recorded on the Navier-Stokes entry; how much of it reaches this unforced result is not clear from the public record, and the credit OpenAI gives to Diego Cordoba and Luis Martinez-Zoroa is stated for the forced program rather than for this one.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Finite-time blowup for the unforced Euler equations from smooth compactly supported data. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-08-euler-unforced-blowupBibTeX
@misc{whataifound-openai-2026-blowup,
title = {Finite-time blowup for the unforced Euler equations from smooth compactly supported data},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-08-euler-unforced-blowup}
}