VibeMathedMath problems solved with AI
Sign in

Finite-time blowup for the inviscid Boussinesq system with smooth forcing

Does the inviscid Boussinesq system on R2\mathbb R^2 admit finite-time blowup from smooth data with forces that are smooth in both space and time? Córdoba, Laín-Sanclemente and Martínez-Zoroa obtained finite-time singularity for the two-dimensional Boussinesq equation with a force only of class C1,4/3−1−ϵ∩L2C^{1,\sqrt{4/3}-1-\epsilon}\cap L^2, leaving the smooth-force case open.

Result
Proved(see note)
Status
Resolved
AI contribution
AI co-developed
Method
Construction
Field
Fluid dynamics; singularity formation for incompressible flow
Posed by
Diego Córdoba, Antonio Laín-Sanclemente and Luis Martínez-Zoroa, whose multiscale construction reached a force of limited Hölder regularity
Year posed
2025
Years open
1y
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
45 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Yes. Blowup for the inviscid Boussinesq system on R2\mathbb R^2 with forces in C∞(R2×[0,T∗])C^\infty(\mathbb R^2\times[0,T_*]) in both equations, supported in one fixed spatial ball, from smooth compactly supported initial temperature and zero initial velocity. The temperature stays bounded while ∥∇θ(t)∥∞→∞\|\nabla\theta(t)\|_\infty\to\infty and the vorticity norm has infinite limsup as t↑T∗t\uparrow T_*. The solution is smooth on every closed interval before blowup and unique in a finite-energy Lipschitz class. This lifts the force from barely C1C^1 to fully smooth, and is the construction the Euler paper then builds on. 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)." The statement continues that after iterating with Claude and Codex on alternative proof architectures, "leading to several different proofs, we arrived at the current simplified argument, which we then iterated on using Claude and Codex, first 5.6 Sol and then Astra once we had access, to arrive at the current writeup modulo our hand editing", and that intermediate writeups were generally fed to Codex "for simplification, ideation, and iteration". Co-developed rather than discovered: the first blowup solution came from Claude, but the multiscale mechanism is Córdoba and Martínez-Zoroa's and the authors fed in their own earlier IPM work.

Verification

Formalised in Lean 4 in tristanbuckmaster/fluid_lean, twice over: boussinesq-blowup carries the general theorem and affinecore the normalised construction with explicit odd initial data. Checked here on 8 September 2026 by reading both READMEs: in each, Challenge.lean is the only file a reader must trust, no other file contains a sorry, the proof rests on no axiom beyond propext, Classical.choice and Quot.sound, and leanprover/comparator is configured to type-check the statement independently and confirm the solution inhabits exactly it. Not peer reviewed. Tao's public commentary describes the Boussinesq case as the model case whose amplitude-frequency dynamics reduce to "a remarkably simple ODE", but records that he is still working through the arguments.

Sources

Changelog1 change

Discussion