VibeMathedMath problems solved with AI
Sign in

Finite-time blowup for the 3D incompressible Euler equations with smooth forcing

Can a solution of the three-dimensional incompressible Euler equations on R3\mathbb R^3, started from smooth data and driven by a force that is smooth in space and time up to and including the blowup time, lose regularity in finite time? Finite-time singularity formation from genuinely smooth data is the central open question for the equations. Elgindi obtained blowup for C1,αC^{1,\alpha} solutions in 2021, and Córdoba and Martínez-Zoroa built a multiscale program producing forced blowup for related equations with forces of limited regularity, but no construction reached three-dimensional Euler with a space-time smooth force. Note on the forced formulation, since it is easy to misread: alternatives (C) and (D) of Fefferman's Clay problem description do permit a smooth force obeying rapid space-time decay, so forcing is not a dodge and the forced route is a genuine path to the prize. It is a path for Navier-Stokes with viscosity, however, and not for Euler, which Fefferman's description excludes from the prize list.

Result
Proved(see note)
Status
Resolved
AI contribution
AI co-developed
Method
Construction
Field
Fluid dynamics; singularity formation for incompressible flow
Posed by
Classical; the breakdown question is recorded in Fefferman's official Clay problem description, which notes it is open and important for Euler though not itself a prize problem
Year posed
2000
Years open
26y
Solved
2026-09-08
Model
Claude, Codex with GPT-5.6 Sol
Vendor
Anthropic / OpenAI
Collaborators
Levent Alpöge, Tristan Buckmaster
Verification
Lean-verified
Publication
Preprint
Significance
70 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Yes. Theorem 1.1: for every r0>0r_0>0 and z0z_0 there are a time T∗>0T_*>0, a divergence-free axisymmetric u0∈Cc∞u_0\in C_c^\infty supported in a fixed solid torus with nonzero swirl and zero meridional velocity, and an axisymmetric force f∈C∞(R3×[0,T∗])f\in C^\infty(\mathbb R^3\times[0,T_*]) supported in that torus, with a solution smooth on [0,T∗)[0,T_*) for which circulation and meridional velocity stay bounded while ∥∇Γ(t)∥∞\|\nabla\Gamma(t)\|_\infty and ∥ω(t)∥∞\|\omega(t)\|_\infty tend to infinity and ∫0T∗∥ω(t)∥∞ dt=∞\int_0^{T_*}\|\omega(t)\|_\infty\,dt=\infty, so the blowup is genuine by Beale-Kato-Majda. It is unique among divergence-free locally space-time Lipschitz solutions with the same data, and competitors need not be axisymmetric. Not the Clay Millennium problem: that problem is Navier-Stokes with viscosity, and Fefferman's official description states that the Euler equation "is not on the Clay Institute's list of prize problems".

What the AI did

The Boussinesq paper devotes its section 2 to an "AI statement": "We happily used both Claude and Codex to iterate on our proof. We had, using Claude, our first blowup solution, but not this one, on 8/15/26, and we Lean verified it on 8/22/26. This involved inputting ideas from previous joint work of ours on blowup for the IPM equation following Córdoba-Martínez-Zoroa and a number of other works of ours and others, as well as iteration with the model on various ansätze, eventually leading to blowup in Boussinesq. The first writeup that we produced iterating with Claude was, in our opinion, the worst writeup we had ever seen in the history of mathematics (topped soon after by the writeups for 3d Euler and then for hypodissipative Navier-Stokes)." Buckmaster's public statement adds that the models used were "Anthropic's Claude, OpenAI's Codex, especially with GPT-5.6 Sol and, more recently, Astra", the last "only used for writeups and auditing our arguments", and that "the first LLM generated proof Levent sent me was the most horrendous I have ever read". He is explicit that the program is not the models': "The credit for the basic idea of this program goes to Diego Córdoba and Luis Martínez-Zoroa... We took their work as a starting point, using Large Language Models to push their program to completion." Co-developed rather than discovered on that account. The Euler paper carries no AI statement of its own.

Verification

Formalised in Lean 4 in tristanbuckmaster/fluid_lean (euler-blowup). Checked here on 8 September 2026 by reading the repository: Challenge.lean states the theorem against plain Mathlib and is the only file a reader must trust, Solution.lean derives it from the development, and comparator.json configures leanprover/comparator to type-check the statement independently, confirm the solution inhabits exactly that statement, restrict axioms to propext, Classical.choice and Quot.sound, and replay the proof. Mathlib is pinned by commit; the build is roughly 1,100 modules and the README warns it needs on the order of 100 GB of memory. The Lean statement was read and matches the paper's Theorem 1.1, including the divergence of the Beale-Kato-Majda vorticity integral and uniqueness against non-axisymmetric competitors. Not yet peer reviewed: Terence Tao has publicly analysed the result and calls it "a remarkable achievement", but says he is still digesting the proof, so no expert has certified the argument line by line.

Sources

Changelog1 change

Discussion