Claimed AI-led

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

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 $\mathbb{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 $\mathbb{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 $\mathbb{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, though less than this entry first said. The Euler challenge module does record an outside source: its header, present since its first commit on 2026-09-08, says it is adapted from Formal Conjectures' Navier-Stokes statement specialized to zero viscosity and zero force, and vibemathed compared it line by line and found the retained conditions match. That anchors the first compared theorem, the breakdown alternative. The second, exists_compact_smooth_euler_singularity, is OpenAI's own richer form of the paper's Theorem 1.1 with no outside counterpart, and a reader checking this should start by reading that statement 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.

Independent checks

vibemathed.com statement audit: Compared ComparatorChallenges/Euler.lean line by line with Formal Conjectures' Navier-Stokes file at 8bf45ed with viscosity and force set to zero and found the retained conditions match for the first theorem; the second theorem is OpenAI's own. Counted no sorry and no axiom declarations under Euler/. Not rebuilt; no mathematician has read the argument. · link ↗

Also recorded at

vibemathedfinite-time-blowup-for-the-3d-incompressible-euler-equations-unforced

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

History of this entry

2026-09-24CorrectedCorrected the caveat, which said the repository records no outside source for the Euler challenge statement. Its header has named Formal Conjectures' Navier-Stokes file as the source since the first commit; only the second compared theorem is OpenAI's own. source ↗
2026-09-24CheckedRecorded vibemathed's line-by-line comparison of the first compared theorem with Formal Conjectures. No grade moved. source ↗
2026-09-22CorrectedRecorded the vibemathed record for this result as a registration. It cites the same theorems and the same repository already sourced here. No grade moved. source ↗
2026-09-10AddedEntered 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.

Community discussion

Hacker NewsOn the Navier-Stokes Millennium Prize Problem↗Hacker NewsHow an AI math breakthrough ignited a controversy↗

Graded claimed for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

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-blowup

BibTeX

@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}
}

Related findings

ClaimedFinite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and DOpenAI · 2026-09-08 ClaimedFinite-time blowup for the IPM equation with uniformly space-time smooth forcingIndependent · 2026-09-15 Formally verifiedOptimal packings of one to seven unit squares in a circle, proved in LeanIndependent · 2026-10-02

pde fluid-dynamics euler-equations singularity lean formalization argument

← All mathematics findings in the registry