The Forced Singularity

Newton’s second law, and nobody knows if it holds

The Navier–Stokes equations are just f = ma written for a parcel of incompressible fluid. Every weather model, every large-eddy simulation of a street canyon, every wind-tunnel comparison is a discretisation of these five lines:

What nobody has been able to settle since Leray’s work in the 1930s is whether a smooth starting state stays smooth forever. Short-time smoothness is classical. Two-dimensional smoothness is classical. In three dimensions the possibility remains that velocity gradients run away to infinity at some finite time — a singularity, or blow-up — after which the equations simply stop having a solution.

This is not a pedantic worry. Blow-up would mean the model of a fluid we use everywhere contains a mechanism that manufactures infinite shear out of finite energy, and that every simulation which appears to resolve small scales is resolving something the continuum equation cannot support. Fefferman’s official problem statement is blunt about why numerics cannot settle it: many computations “appear to exhibit blowup”, but “the extreme numerical instability of the equations makes it very hard to draw reliable conclusions”.

Four statements, and you only have to prove one

The Clay Mathematics Institute did not pose one question. To give, in Fefferman’s words, “reasonable leeway to solvers while retaining the heart of the problem”, the official statement offers four propositions and asks for a proof of any single one of them. Two assert eternal smoothness with no force applied. Two assert breakdown, and those two explicitly permit a force — any smooth f that decays fast enough.

Here is the point that most of the coverage has skated over, and it is a logical one rather than a physical one. (C) is not the negation of (A). (A) speaks about the unforced equation; (C) speaks about the forced one. You can prove (C) and leave (A) entirely intact — both could be true at once. So the letter of the prize can be satisfied while the question everyone actually cares about, whether a fluid left alone can destroy itself, remains exactly as open as it was on 7 September.

Charles Fefferman, who wrote the problem, put the physical distinction plainly to Quanta: with a force, the singularity is something done to the fluid; without one, it is the fluid doing the crazy stuff by itself. He was, all the same, delighted — “I was thrilled that the problem was solved.”

An infinite cascade, paid for by the force

The construction is not a clever exact solution. It is an infinite regress, and it belongs to Diego Córdoba and Luis Martínez-Zoroa, who found it for a simpler model. You take a perfectly well-behaved solution, then add a small correction at a finer scale that makes it slightly more singular near a target time. Then another, finer and smaller. Then another. Amplitudes shrink, but length scales shrink faster, so the ratio between them — the velocity gradient, the vorticity — grows without bound as the target time is approached.

Each correction leaves an error in the momentum balance. The forcing term is what absorbs it. That is why the force is not decoration: it is the ledger the whole cascade is charged to. And it is why the hard part was never blow-up itself but smoothness — getting every stage of an infinite stack to close with a force that is C^∞ and decaying, rather than merely rough.

In mid-August, Levent Alpöge and Tristan Buckmaster found a variant of the cascade that pushed smooth forcing through three equations at once: the incompressible porous-medium equation, two-dimensional Boussinesq, and three-dimensional Euler. They formalised all three in Lean. Terence Tao, writing on 7 September, called it remarkable, noted the arguments were “heavily AI-assisted”, and said he saw no fundamental obstacle to carrying the method to Navier–Stokes. He also relayed a verdict on the first write-up that will outlive the result itself: “the worst writeup we had ever seen in the history of mathematics”.

Viscosity is the remaining step. Euler is scale-invariant in a way that lets a cascade concentrate freely; the Laplacian in Navier–Stokes smears every fine scale you build, and it smears the fine ones fastest. Closing that gap — making a cascade outrun its own dissipation — is what OpenAI says its agents did over one weekend. Its manuscript describes the resulting flow as a vortex spiralling inward while stretching along its axis, with acceleration, pressure gradient, advection and dissipation all growing enormous while cancelling each other almost exactly.

Eighty-eight hours, and a receipt

OpenAI ran an unreleased internal model — described only as significantly more capable than GPT‑6 Astra, and in training since 28 August — as a swarm of roughly ten thousand concurrent agents. They started on 1 September and had an analytical proof on 5 September. GPT‑6 Astra then formalised it in Lean 4 in a further seventeen hours.

The Lean formalisation is the part that deserves attention. A 166-page analytic argument produced by a machine is, epistemically, a difficult object: nobody has read it, and a subtle local error in an infinite construction is exactly the kind of thing that survives a first reading. A Lean certificate changes the question from “do we trust the author” to “do we trust the statement at the top of the file”. A formal proof cannot be talked into looking correct — which matters rather more when the author is a model with a marketing department.

So the correctness question is close to settled, and the interesting questions are all about what was proved and who got there first.

Two labs, three weeks, one rumour

The human result came first, on a neighbouring problem, and was itself AI-assisted — by Anthropic’s models, in Alpöge’s and Buckmaster’s hands. What happened next is disputed on almost every point except the dates.

The provenance question

Buckmaster asked whether his own Codex sessions — the mathematics he was working through on OpenAI’s product while the write-up was still private — could have reached the model. Chief Research Officer Mark Chen’s denial is precise and worth reading twice: “no people or AI systems searched user data to solve the problem.” That answers retrieval. It does not answer training, and OpenAI has reportedly declined to rule out that anonymised product usage contributed to the model’s capability.

Buckmaster has been careful to say he makes no accusation, and generous about the mathematics: he thinks Martínez-Zoroa deserves a Fields Medal. Fefferman calls Córdoba and Martínez-Zoroa “the heroes of the story”. Both are pointing at the same thing — the idea was human, and old.

What Tao objects to

Tao’s complaint is not about correctness. It is that famous problems are becoming proof points for model launches. He had hoped AI in expert hands would be an instrument — a microscope for a biologist, a telescope for an astronomer — and finds it increasingly used autonomously to emit answers with little insight attached. He has also had to correct people reading his praise of the Euler work as confirmation of something that has not happened: unforced global regularity is still open.

The Clay Institute has certified nothing, and its rules make that structural: a solution must appear in a peer-reviewed journal of high standing and then survive two years of scrutiny. Its president, Martin Bridson, offered only that it is “certainly an exciting day, as we contemplate the announcement of major advances in the human understanding of mathematics”.

What you can now say, and what you cannot

Why this matters for people who run these equations

Almost nothing changes numerically, and that is the honest answer. Nobody’s LES was unstable because of statement (C), and the forcing terms in an urban canopy run — buoyancy, pressure gradient, canopy drag — are not cascades engineered to pump gradients at 2^−k scales. What changes is the epistemics of the field around you. A hard analytic result now arrives as a Lean repository from an anonymous model, with a priority dispute attached and a company’s launch schedule behind it, and the pieces mathematicians normally trade in — insight, attribution, a readable argument — are the pieces that came out worst.

The one durable lesson is about verification. Alpöge and Buckmaster shipped Lean alongside an admittedly unreadable draft, and that is why their claim was credible within a day rather than a year. When a machine is the author, a formal certificate is not pedantry; it is the only part of the submission that cannot be spun.