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.

The argument moved off the mathematics

In the eight days since this page was compiled, very little has happened to the proof and a great deal has happened around it. The Lean repository gained twenty-five thousand lines and then went quiet. The Clay Institute opened a process. Three learned societies put out statements that disagree with one another about what had just occurred. And twenty-five Fields Medallists signed a declaration that names neither OpenAI nor Navier–Stokes and is unmistakably about both.

What the repository shows, checked on 17 September

The Lean certificate is the one part of this story that can be inspected rather than reported, so it was inspected. Two commits exist. The second, on 10 September, added 25,143 lines across some two thousand six hundred files — which means the release of 8 September, the one every outlet described as machine-checked, was not yet the finished formalisation.

Scale

2,659 .lean files, 641,332 lines, 47 MB.

Axioms

No axiom declaration anywhere in the tree. Nothing is asserted without proof.

Holes

Five occurrences of sorry, all inside ComparatorChallenges/, where the file’s own header calls them “intentional sorry challenge placeholders”. They are the goal the proof must meet, not a gap in it.

The target statement

Not OpenAI’s own. It is copied, with the upstream commit pinned, from Google DeepMind’s Formal Conjectures rendering of Fefferman’s (C) and (D), and the header records that “neither the proof root nor the submission imports this reference”.

What that statement demands

globally_bounded_energy — Fefferman’s finite-energy condition (7) — decay of the force in every derivative, and, on the torus, periodic pressure “following the errata appended to the Clay problem statement”.

Who signed it off

The repository ships a formalization.yaml declaring each result sorry_count: 0 on the three standard classical axioms (propext, Classical.choice, Quot.sound) — and, at line 104, a field that has not changed since 8 September: review: status: “self-assessed”.

Toolchain

Pinned to lean4:v4.34.0-rc2, a release candidate. The mathlib revision is pinned too, and is now behind the toolchain Comparator itself has moved to.

What is missing

Issues are disabled on the repository. There is no CI workflow. No rebuild by anyone outside OpenAI has been published.

What the 10 September commit changed was the route rather than the completeness. The 8 September tree already closed (C) and (D) with no sorry, but through an assembled candidate; the new files re-point both top-level theorems at the manuscript’s own named results, so that what the Lean proves and what the paper claims are the same object rather than two objects that agree. That is a real improvement, and it is also not what anyone was told had already happened on the 8th.

The first six entries are stronger than the coverage suggested: checking a machine’s proof against a statement written by a rival laboratory, in a file the proof cannot see, is close to the best available answer to “but does the Lean theorem say what Fefferman said”. The sixth is the counterweight, and it has not moved in nine days. A certificate that checks is not the same thing as a certificate that has been checked by someone with no stake in the answer.

Nor has anyone qualified said in public that they have read the manuscript and believe it. The two analysts closest to the construction gave a joint interview to El País on 10 September, and what they said was about provenance, not correctness. Luis Martínez-Zoroa, whose cascade the proof extends, had not yet read the 166 pages closely: parts of it reminded him of the strategies they had developed, the notation was unfamiliar, and until he had worked through it properly he could not say how heavily it leaned on their method. Diego Córdoba was blunter about what had actually been contributed — “si nuestro trabajo no hubiera existido, la IA no habría resuelto el problema”, and what the machine did was “ganar tiempo, no tener ideas nuevas”. María Victoria Otero, president of the Spanish Royal Mathematical Society, put it plainly three days later: without Córdoba and Martínez, there would be no proof.

The one senior figure to assert the theorem as established in this window is Timothy Gowers, in passing on 17 September, with his own OpenAI connections disclosed, and he is not a fluids specialist. Nine days after the announcement, the set of people who have both the expertise to referee this construction and a public position on whether it is correct is still empty. The man whose idea it was had not finished reading it.

A third bucket, holding one problem

Clay’s statement of 11 September names nobody — not OpenAI, not Buckmaster, not Alpöge — and says the problem “has apparently been settled”, that it hopes to see the work “analysed and interrogated”, and that its own rules cover “evaluating what has been achieved and for assigning credit”. That last clause is the priority dispute, acknowledged without being mentioned.

The more telling change is not in the prose. The Millennium Prize Problems index now sorts the seven into three groups where there were two:

“Active” is a category that did not exist before this month, and it holds exactly one problem. Navier–Stokes is now in neither of the two buckets an institution normally has. That is what an institution does when the honest answer is longer than a heading — and it is a more candid account of the position than anything in the statement it published the same day.

Four statements, machine-readable

There is a tidier answer to “what exactly was settled” than any press release gave, and it is sitting in a rival laboratory’s source tree. DeepMind’s Formal Conjectures project carries all four Clay alternatives as Lean statements, each tagged with its research status. As of today, the file reads:

Two solved, two open, annotated by a rival laboratory rather than by the claimant or the prize-giver, with the citation pointing at OpenAI’s commit of 8 September. It is the whole argument of this page in four attributes, and a cleaner statement of the position than the Clay Institute, the AMS or the EMS has managed in prose. It is not, however, an independent verification: DeepMind reclassified on the strength of the commit existing, not of having rebuilt it.

Still not on arXiv

Neither OpenAI’s two manuscripts nor the three Alpöge–Buckmaster preprints are on arXiv as of 17 September. The OpenAI papers are PDFs on a content-delivery network; the others were posted to Mastodon and to a personal page. An arXiv identifier for the Alpöge–Buckmaster work circulated widely enough to reach several summaries of this story, and resolves to an unrelated paper on conformal Ricci curvature. The entire corpus in the biggest result of the year currently sits outside the channel the field uses to timestamp and preserve work.

A denial that narrowed four times

The most substantive movement of the week is not in anything anyone said about 6 September. It is in what OpenAI has been willing to assert about its own training data, which changed shape four times in six days and travelled a long way.

Read as a sequence this is a real concession being made in reverse. The first statement conceded that de-identified usage data might have helped and asked to be trusted that it did not matter; the last names a date before which the pretraining corpus was closed, which is a claim that could be falsified by anyone with access to the training logs. Nobody outside the company has that access, and no external audit has been offered. But a company that says “3 July” has staked something that a company saying “nobody searched user data” had not.

Buckmaster rejected the accompanying accounts flatly on 10 September, and the wording is his alone: Sébastien Bubeck’s statement was “wildly false”, no apology was ever offered, and rather than retract the remark Bubeck “doubled down on his threat” — “if you don’t want me to be nice, then i don’t have to be nice”. Bubeck’s own last word on authorship remains his post of 8 September: “I never ever asked for Levent to be removed from authorship of his own work” — a sentence about Alpöge’s own paper, which is not the document the allegation concerns. Since 13 September neither side has said anything further.

A correction, and a second front

This page’s account of 8 September had a gap. OpenAI released two papers that day, not one. Beside the Navier–Stokes manuscript sits a separate Euler paper, and its claim is not about a forced equation at all: a smooth, compactly supported, divergence-free velocity field on ℝ³ whose solution to the unforced incompressible Euler equations develops a singularity in finite time, with the C¹ norm unbounded and the time integral of ‖ω‖_∞ divergent — the Beale–Kato–Majda criterion, failing.

And on 7 September, the same day Buckmaster went public, Anima Anandkumar’s group at Caltech posted a self-similar unforced Euler blow-up on ℝ³ reached by an entirely different route: physics-informed neural networks to find the approximate profile, spline representations to turn it into certified bounds. Two independent attacks on the same unforced target, three days apart, by methods with nothing in common.

None of this touches (A) or (B). Euler is not Navier–Stokes, and the sentence in § 03 — that viscosity is the remaining step — was written about the forced cascade and still stands for it. But the unforced problem is no longer quiet, and the place to watch is now the inviscid one.

Why the letters read the way they do

The Fields declaration never mentions a company or an equation. Its complaint is about what a proof is for: “solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight”, and against that, results “announced in a rush, leaving no time for a proper writeup, the isolation of new methods and ideas, and citing relevant previous work”. Tao signed it and conceded the haste: “we did not have the time to have a more consultative process… the urgency of the situation was such that we needed to release a statement sooner rather than later.”

The societies split. The EMS put the access problem first — “the model used in this current situation is internal to OpenAI and not generally accessible”, which it calls a major problem for the community — and insisted the result “does not come out of a vacuum”, naming Córdoba, Martínez-Zoroa, Zheng, Alpöge and Buckmaster. The AMS took the opposite tone, tracing a single line from Navier and Stokes through Leray and Ladyzhenskaya to Córdoba and Martínez-Zoroa, then Alpöge and Buckmaster, “with the final steps taken by OpenAI mathematicians”. Clay said only that the problem has “apparently been settled” and that its own process is “deliberately unhurried”. It has said nothing at all about forced versus unforced.

The London Mathematical Society, first out on 9 September, split the difference and got closest to what the mathematicians themselves went on to say: a remarkable achievement, and a reminder from its president Mark Chaplain that “while new AI tools can greatly accelerate exploration and discovery, the goal remains human understanding”.

The sharpest dissent is internal. Timothy Gowers declined to sign, not over capability but over the hierarchy the letter assumes: “there is a spectrum of attitudes in mathematics to the relationship between problem-solving and conceptual understanding”, and he did not want to imply his own end of it was the wrong one. His worry is structural instead — whether young mathematicians stay motivated once problem-solving stops conferring standing.

Math slop causes technical debt in mathematics, and in some ways it’s even more insidious.

Henry Cohn, 15 September

Cohn’s essay does not mention Navier–Stokes; his example is Mochizuki. That is what makes it the most useful thing written this week. A correct proof nobody can absorb is a liability the field carries, and the question a Lean certificate cannot answer is who now owes the exposition.