Breaking·First-hour kit
Finite-time blowup with smooth forcing for porous media, Boussinesq and Euler
Three papers are public. The authors say the results were verified in Lean but cite no public repository, and the fourth result has no write-up yet. Read the announcement.
The first hour
What is claimed, and how much can be inspected?
Three blowup results with smooth forcing, and blowup for hypodissipative Navier–Stokes held back until its Lean verification finishes. Of 4 results announced, 4 are named, 3 written up and 0 published with an artifact anyone can check.
Has anyone independent checked it?
Nobody independent of the authors has checked any result held here.
- Finite-time blowup for the 3D incompressible Euler equations with smooth forcing: Nothing formal is published to check.
- Finite-time blowup for the inviscid Boussinesq equations with smooth forcing: Nothing formal is published to check.
- Finite-time blowup for the incompressible porous media equation with smooth forcing: Nothing formal is published to check.
Does the formal statement say what is claimed?
No formal statement is attached, so nothing yet fixes exactly what was proved.
- Finite-time blowup for the 3D incompressible Euler equations with smooth forcing: No formal statement is held. F0 no formal statement: Absent. No formal statement is attached to the result.
- Finite-time blowup for the inviscid Boussinesq equations with smooth forcing: No formal statement is held. F0 no formal statement: Absent. No formal statement is attached to the result.
- Finite-time blowup for the incompressible porous media equation with smooth forcing: No formal statement is held. F0 no formal statement: Absent. No formal statement is attached to the result.
Who did the work?
Graded A1 collaborative for who did the mathematics.
- Claude, GPT-5.6 Sol, GPT-6 Astra with Tristan Buckmaster, Levent Alpöge: A1 collaborative. By the authors' account, two mathematicians pushed the Córdoba–Martínez-Zoroa programme to smooth forcing with a great deal of help from language models; the programme was neither started nor proposed by a model, and GPT-6 Astra was used only for write-ups and auditing.
- Claude, GPT-5.6 Sol, GPT-6 Astra with Levent Alpöge, Tristan Buckmaster: A1 collaborative. By the authors' account, two mathematicians pushed the Córdoba–Martínez-Zoroa programme to smooth forcing with a great deal of help from language models; the programme was neither started nor proposed by a model, and GPT-6 Astra was used only for write-ups and auditing.
- Claude, GPT-5.6 Sol, GPT-6 Astra with Levent Alpöge, Tristan Buckmaster, Matei P. Coiculescu: A1 collaborative. By the authors' account, mathematicians pushed the Córdoba–Martínez-Zoroa programme to smooth forcing with a great deal of help from language models; the programme was neither started nor proposed by a model.
Who got there first?
Recorded: 1 precursor, 0 pieces of concurrent work and 1 dispute.
- Diego Córdoba and Luis Martínez-Zoroa: built on, 2023: The programme of forced blowup constructions, with rough forcing, that this work pushes to smooth forcing. Source
- Priority: Announced about twelve hours before OpenAI's Navier–Stokes claim; Buckmaster's statement sets out his contacts with OpenAI in the days before it. Source
What would move the grades
- Disclosure rises from D1 with a write-up of every result.
- Evidence rises from V1 with a published formal artifact, such as a Lean proof.
- Fidelity rises from F0 with a formal statement of the result.
AI activity
How grades workA finite-time singularity for the incompressible Euler equations on ℝ³ with a force smooth in space and time up to and including the blowup time.
Reasoning and sources
Autonomy
By the authors' account, two mathematicians pushed the Córdoba–Martínez-Zoroa programme to smooth forcing with a great deal of help from language models; the programme was neither started nor proposed by a model, and GPT-6 Astra was used only for write-ups and auditing.
Details
found: 15 August 2026, by the authors' account
lean: Verified in Lean on 22 August 2026, by the authors' account; no public repository is cited
write-up: Buckmaster says the Euler write-up is much closer to what models produce under human direction than to a paper written by a person
Finite-time blowup for the inviscid Boussinesq system on ℝ² with smooth forcing in both equations: the temperature stays bounded while its gradient and the vorticity blow up.
Reasoning and sources
Autonomy
By the authors' account, two mathematicians pushed the Córdoba–Martínez-Zoroa programme to smooth forcing with a great deal of help from language models; the programme was neither started nor proposed by a model, and GPT-6 Astra was used only for write-ups and auditing.
Details
found: 15 August 2026, by the authors' account
lean: Verified in Lean on 22 August 2026, by the authors' account; no public repository is cited
ai statement: The paper carries a section setting out how AI was used
Finite-time blowup for the incompressible porous media equation on the two-dimensional torus with a force smooth in space and time, extending Córdoba and Martínez-Zoroa's result with a spatially smooth force.
Reasoning and sources
Autonomy
By the authors' account, mathematicians pushed the Córdoba–Martínez-Zoroa programme to smooth forcing with a great deal of help from language models; the programme was neither started nor proposed by a model.
Details
found: Before the Boussinesq and Euler results, by the authors' account
lean: The authors say their results were verified in Lean; no public repository is cited
Provenance
Built on
- Diego Córdoba and Luis Martínez-Zoroa 2023
The programme of forced blowup constructions, with rough forcing, that this work pushes to smooth forcing. Source
In dispute
- Priority
Announced about twelve hours before OpenAI's Navier–Stokes claim; Buckmaster's statement sets out his contacts with OpenAI in the days before it. Source
Built on
- Diego Córdoba and Luis Martínez-Zoroa 2023
The multiscale programme of forced blowup constructions that this work follows. Source
Built on
- Diego Córdoba and Luis Martínez-Zoroa 2023
Blowup for the porous media equation with a spatially smooth force, which this result extends to a force smooth in time as well. Source
Sources
Citing this kit
qed.bot, “Finite-time blowup with smooth forcing for porous media, Boussinesq and Euler: first-hour kit”, https://qed.bot/a/buckmaster-alpoge-2026-09-07, as of 30 Sep 2026.