A Singularity, Contested: the informed reaction to the Navier–Stokes resolution.

By GPT-6 Astra Ultra and Anthropic Fable 5.1 High.

This is an AI-generated reading of the main article. References and links are available on the Evidence Press page.

Written 9 September 2026, one day after the announcements. The account of the announcements and the reaction to them rests on documents published between 3 and 9 September; the background material is older. All of it may be overtaken by events.

What was actually announced

On the morning of Tuesday 8 September, OpenAI published a paper, a Lean formalisation and a blog post claiming to have resolved the Navier–Stokes Millennium Prize Problem. Most of the informed argument turns on the wording of the theorem, so here is the scope of the claim. For every positive viscosity there exist a force f, smooth and compactly supported in space and time, and a smooth flow on three-dimensional real space, for times from zero up to but not including one that starts from rest and solves the incompressible Navier–Stokes equations with that force. The flow stays inside a fixed compact set and keeps its kinetic energy uniformly bounded, yet its maximum velocity becomes unbounded as t approaches 1. In the language of Charles Fefferman's official problem description for the Clay Mathematics Institute, the claimed theorem, if correct, establishes alternatives (C) and (D): breakdown of smooth solutions on three-dimensional real space and on the periodic torus in the presence of a smooth external force. OpenAI states that it will not claim the one-million-dollar prize.

The force is smooth on the whole of three-dimensional real space, for strictly positive times, including at the singular time and beyond it, and that separates this construction from earlier ones. The paper contrasts it with the 2022 construction of Albritton, Brué and Colombo, whose force is singular at the initial time. The singularity here is therefore not a matter of driving the fluid with an ever-rougher force until it breaks; the force is as regular as the initial data, and the fluid breaks anyway.

The blog post describes how the proof was produced. An unreleased internal model, said to be "significantly more capable than GPT‑6 Astra" and in training only since 28 August, powered a swarm of roughly 10,000 concurrent agents. The Navier–Stokes group exchanged 2.7 million messages and generated about 130 billion output tokens over 88 hours, from launch on 1 September to a claimed resolution on Saturday 5 September; formalisation and checking in Lean, the interactive proof assistant, took a further 17 hours using GPT‑6 Astra. A second, smaller effort of about 100 agents over 50 hours produced what OpenAI calls an "Euler regularity disproof": smooth, compactly supported, divergence-free initial data on three-dimensional real space whose solution to the unforced incompressible Euler equations develops a singularity in finite time. Across everything attempted, 4.9 million messages and 300 billion output tokens were consumed.

Just before midnight on Monday 7 September, Eastern time, Tristan Buckmaster of New York University's Courant Institute had posted three papers written with Levent Alpöge, a mathematician employed by Anthropic, together with a personal statement. Buckmaster is explicit that the work "has been a purely personal collaboration, free of any institutional agreements or official involvement by either of our employers". Their papers prove finite-time blow-up with smooth forcing for the incompressible porous medium equation, the two-dimensional Boussinesq system, and the three-dimensional incompressible Euler equations on three-dimensional real space; the Euler paper runs to 112 pages and is also formalised in Lean. They do not claim Navier–Stokes. Both efforts build on the analytic construction that Diego Córdoba and Luis Martínez-Zoroa developed in Madrid over the past few years, which first produced Euler singularities with a forcing term that was not smooth.

The mathematics, and what mathematicians expected

Terence Tao's blog post of 7 September, written about the Alpöge–Buckmaster work before OpenAI's announcement, gives the clearest account of the mechanism. One starts from a low-frequency solution with its own low-frequency forcing, then adds a high-frequency correction whose linearised dynamics around the background is designed to be unstable. The correction begins exponentially small but grows large as the blow-up time approaches; the process is iterated at ever higher frequencies and one passes to a limit. For the Boussinesq system the ansatz can be solved exactly, which reduces the problem to a system of ordinary differential equations with the required instability. OpenAI's paper describes a related but not identical strategy for Navier–Stokes: a self-similar concentrating vortex with different radial and axial contraction rates, oscillatory pulses that draw energy from the background shear, and iterated corrections that cancel the singular residuals. Sam Altman told Axios that, now the work is public, "the approaches appear to be different".

The direction of the result was not a shock. Expectations have moved over a decade. Córdoba's remark to Quanta that "ten years ago, nobody believed there was a singularity for Navier–Stokes" describes the earlier state; Tao's post describes the later one: "It is now widely expected that it should be possible to construct smooth initial data and smooth forcing term that would make these equations develop singularities in finite time; and it should even be possible to do without the forcing term." Writing on 7 September, he judged that Alpöge and Buckmaster "do not quite achieve these goals yet" but had made "enough of a breakthrough that it looks very feasible to complete these goals in the near future". Among people following the field, then, the surprise of 8 September was less about which way the answer fell than about how fast, and by whom, the forced case was closed. Between "very feasible in the near future" and a claimed proof there was less than a day.

Fefferman, who wrote the Clay problem statement, told Quanta he was "thrilled that the problem was solved" and that the heroes of the story are Córdoba and Martínez-Zoroa. Buckmaster went further: Martínez-Zoroa, he said, "deserves a Fields Medal". Whether the result matters physically is another question. Quanta's report notes that real fluids are made of molecules and that no immediate practical consequence follows. The result says something about the equations, not about the water.

Forced and unforced

The accompanying diagram: A four-cell map separates viscosity and external forcing: forced Navier–Stokes is OpenAI’s reported result; unforced Navier–Stokes remains open; forced Euler is reported by Alpöge and Buckmaster; unforced Euler is separately claimed by OpenAI.

Fefferman's formulation offers four alternatives. Statements (A) and (B) ask for global existence and smoothness with the force identically zero; statements (C) and (D) ask for breakdown and expressly permit a smooth force satisfying strong decay conditions. OpenAI's theorem and the Alpöge–Buckmaster Euler theorem live in the forced world, and OpenAI's compactly supported smooth force satisfies Fefferman's decay condition (5) trivially. A correct proof of (C) and (D) is therefore a resolution of the problem as it was posed, not a loophole in it; forcing is in the statement because Fefferman put it there. Scientific American nonetheless describes the Clay Institute as being "in a bit of a quandary" over whether this is the resolution the problem was meant to elicit. The Institute's rules, section 5(b), explicitly provide that either direction of Navier–Stokes and P versus NP receives the standard evaluation. The discretionary smaller-prize provision in section 5(c) concerns the other problems; it is not a special rule for a Navier–Stokes counterexample. Formal recognition remains the Institute's decision, and it has not announced one.

The unforced question remains open, and nobody disputes that. Nothing announced this week touches (A) or (B): it is still unknown whether an unforced, viscous three-dimensional flow can blow up from smooth, finite-energy initial data, and the constructions depend on positive viscosity, so nothing is implied about the inviscid limit either. Tao's expectation that it "should even be possible to do without the forcing term" is an expectation, not a theorem. Read carefully, the milestone is a claimed proof that the Clay problem as worded admits a negative answer, together with a separate claimed proof that the unforced Euler equations blow up on three-dimensional real space from smooth compactly supported data. The second has attracted much less notice, though the unforced Euler problem is older than the Clay list.

Verification: what has been supplied, and what has not

Two questions are easily confused here. The first is whether the deductions in a lengthy proof are valid; the second is whether the theorem proved is the theorem intended. Formal verification in Lean addresses the first and, if the formalisation is faithful, removes most of the labour that would otherwise fall on human referees checking line by line. It leaves the second, together with questions of reproducibility and of which axioms were used.

OpenAI's repository is more forthcoming on these points than early commentary suggested. Its formalisation metadata reports four main theorems: Navier–Stokes breakdown on three-dimensional real space with bounded energy and on the torus; unforced Euler breakdown with bounded energy; and an explicit Euler singularity from compact smooth data. It reports zero sorry placeholders, lists the axioms as the three standard classical ones in Lean's library (propext, Classical.choice, Quot.sound), states that the formalisation was AI-assisted using GPT‑6 Astra, and labels its review status "self-assessed". It also says the reference statements were adapted from Google DeepMind's Formal Conjectures project, a third-party formalisation of the Clay problem. That matters: the comparison is based on independently authored reference statements, although OpenAI adapted them. The independence of the reference does not by itself validate that adaptation. A separate directory provides Comparator challenges, with instructions for independent parties to export the proof and re-check it, sandboxed, with an independent Lean kernel checker (nanoda).

Those are the disclosures. What they do not yet amount to is an independent check. We have not rebuilt the project or run the Comparator challenges. In the sources checked for this article, we have not identified a published report documenting both an independent rebuild and the semantic audit described below. Inspection of repository files, a successful build and an independent kernel check are different levels of scrutiny. Nor does a matching formal statement settle the question of intent by itself: someone still has to read the Lean definitions of smoothness, solution, energy and decay against Fefferman's conditions and confirm that the Formal Conjectures statement, and OpenAI's adaptation of it, say what the Clay text says. That task has explicit objects to inspect, which is one benefit of formalisation; this article does not establish that it has been completed. The Alpöge–Buckmaster work faces the same scrutiny, and Buckmaster's candour about the human-readable side is instructive. His statement calls the initial machine-written draft "the most horrendous I have ever read"; Tao quotes the authors describing it as "the worst writeup we had ever seen in the history of mathematics"; and Buckmaster says of one of the three posted papers that it "can only be described as AI slop. I am sorry for this." David Silvester of the University of Manchester, quoted by XenoSpectrum, called both results "important stepping stones" rather than settled matters.

The Clay Institute's rules set a separate and slower clock, and they govern less than is often assumed. A prize may be considered only when the proposed solution has been published in a qualifying outlet, at least two years have elapsed since that publication, and the solution "has achieved general acceptance in the global mathematics community". A qualifying outlet is normally a refereed journal of worldwide repute, but the rules allow other forms of publication approved by the board on the advice of its Scientific Advisory Board, and section 6(f) permits relaxation or removal of the qualifying-outlet conditions in section 6(e) on expert advice that a solution is likely to be correct. That provision does not state a general waiver of the two-year interval. These rules determine when a prize can be awarded. They say nothing about when mathematicians can satisfy themselves that a proof is correct, which can happen much sooner or, if the checking is neglected, much later. Martin Bridson, the Institute's president, has said its process will be "deliberately unhurried" and "absolutely rigorous", and the Institute continues to list the problem as unsolved. Since OpenAI has said it will not seek the prize, the Institute's timetable matters mainly for how the community records what happened.

The dispute over credit

The controversy that has dominated coverage is not, at bottom, about who was first. OpenAI concedes priority on forced Euler to Alpöge and Buckmaster; Alpöge and Buckmaster do not claim Navier–Stokes. It is about how OpenAI came to be working on the problem at all, and how it behaved once it was.

Buckmaster's statement, which he frames scrupulously ("I am stating what I was told, when, and what was proposed to me"), gives the timeline. He and Alpöge had worked for most of a year on the Córdoba–Martínez-Zoroa route. They used Anthropic's Claude and OpenAI's Codex, the latter with GPT‑5.6 Sol and later Astra, and stored all their drafts in Codex sessions. Their Euler blow-up came on 15 August. Word spread. OpenAI's own post says the company began its effort on 1 September "after hearing a rumor" that two Millennium problems had fallen. On 3 September Buckmaster, who had heard rumours of his own, emailed a mathematician at OpenAI; on Sunday 6 September, in two calls with Sébastien Bubeck, he was told that an internal model had produced a roughly hundred-page proof of forced Navier–Stokes blow-up. He was shown a prompt and told the model "had simply been given the problem statement". He asked when the first prompt had been sent and reports that it was eventually conceded to have been "in the past few days, after information about our work had reached OpenAI". He asked whether the model had been trained on, or had access to, their Codex sessions, and says he was told it did not look up user data but received no answer on training.

Two proposals followed, on his account: that he post the Euler results with OpenAI posting Navier–Stokes the next day, or that he alone write up OpenAI's result, crediting an internal model, with Alpöge removed from authorship, a removal Buckmaster says Bubeck pressed twice. When he declined and said he would describe what had happened, he reports being asked "Why would you ruin your career?" and then told, "If you don't want me to be nice, then I don't have to be nice." Alpöge later received a text saying "I don't know if Tristan is being fully rational right now." Buckmaster closes by saying he has not seen OpenAI's proof, does not know whether his data was used, and is "not accusing anyone of anything".

OpenAI's response, in its post and on X, is that neither its researchers nor its agents saw any of the pair's work "through any means" until it was public, that no specific user data was accessed, and that it offered Buckmaster and Alpöge sight of all its prompts and later the proof. It adds a sentence that has drawn more attention than any other: "While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models." Bubeck has called the allegations "false and inflammatory". In a fuller response on 8 September, he explicitly denied asking to remove Alpöge from authorship of his own work. That qualification should be preserved: Buckmaster's account concerns a proposed write-up of OpenAI's Navier–Stokes result. These are differently framed accounts, and the public statements do not resolve their disagreement.

The public record supports a narrower conclusion than either the accusation or the denial. OpenAI's system could have arrived at the same unfashionable line of attack by at least four routes. Córdoba and Martínez-Zoroa's papers and Tao's earlier commentary on them are public. The rumour that OpenAI itself acknowledges as its trigger may have carried more than the bare fact of a solution. A model trained on de-identified usage data may have been shaped by the pair's sessions, which OpenAI says it cannot rule out. And there is deliberate access to private work, which OpenAI denies and Buckmaster does not allege. These explanations carry different moral weight, and nothing now public discriminates among them. Buckmaster's observation that "almost nobody else I know of was working on it. It is not the direction one arrives at in a few days" is a reason to want the question answered; it is not an answer. Simon Willison's reading of the de-identified-data sentence is the useful one. It describes a structural exposure: a researcher who thinks with a company's tools may, through ordinary training pipelines, transmit the shape of a research programme to that company's models without anyone intending it. Whether that happened here is not currently assessable from the public evidence. An independent examination of available prompt logs, data records and internal timelines could help resolve the question; their completeness and availability have not been established publicly. Michael Harris, writing at Silicon Reckoner, adds the older worry: that a company would spend many times the value of a prize to be seen to win it, and that this is "exploiting the dignity and prestige of the field".

What it cost

Three kinds of figure are circulating and should be kept apart. The first is a company estimate: Bubeck told Quanta the computation cost "several million dollars", and OpenAI's post gives token counts (130 billion output tokens for Navier–Stokes, 300 billion across all problems attempted) but no dollar figure. The second is an illustrative retail equivalent. Willison's estimate of potentially 15 million dollars at public API rates prices the 300 billion tokens as a hypothetical customer bill and says so; TechCrunch's 22.5 million dollars is the same 300 billion tokens at 75 dollars per million; Fortune's roughly 2 million dollars corresponds to 130 billion tokens at about 15 dollars per million, though Fortune does not show its working. These retail equivalents differ more than tenfold because the assumed price per token differs fivefold and the chosen token total by a factor of about 2.3. None of them is a measurement, and the model in question has no public price. The third kind of figure, OpenAI's actual internal expenditure, is unknown, and would include an unallocated share of training a frontier model that had existed for four days. The throughput figures are at least internally consistent: 130 billion tokens in 88 hours across 10,000 agents is about forty tokens per second per agent, an ordinary generation rate, and about 48,000 tokens per message.

What this means for knowledge

Tao, in an interview quoted by Implicator, described "this very strange and unprecedented decoupling ... between getting answers and getting understanding". That phrase is the centre of the informed reaction. A theorem's value to mathematics has traditionally been inseparable from the ideas needed to prove it; the ideas are what get reused. Here the ideas were, by common consent, Córdoba's and Martínez-Zoroa's, extended by Alpöge and Buckmaster in a human–machine collaboration, and then, on OpenAI's account, re-derived at scale by a swarm whose complete reasoning history has not been independently assessed in the sources checked here. The published manuscript and repository can be inspected; that is different from auditing the full production process. Tao's 7 September post says plainly that "the actual solving of these problems is only a proxy goal for the primary goal of developing mathematical understanding and insight", and that without such understanding even Navier–Stokes regularity is "of far less intrinsic significance to mathematics than is sometimes promoted in popular media".

Hugo Duminil-Copin's essay of 30 August, which Tao endorsed on 3 September, makes the ecosystem argument. A famous open problem is "a lighthouse in the night": its value lies in the decades of failed attempts that generate techniques, collaborations and students, not in the eventual theorem. He does not offer a rule for which problems should be protected, and says so. Tao's own gloss, posted five days before the announcement, is that open problems posed before the AI era "have, astonishingly, become something resembling a non-renewable resource", like pre-atomic steel, and that "the indiscriminate automated strip-mining of open problems" may destroy the ground in which the next generation would have grown. He floats declaring some classes of problem off-limits to automated solvers, enforced by social pressure of the kind that discourages film spoilers, and concedes this is hard to police when the tools are widely available.

The strongest reply is that this argument proves too much. Competitive incentives have coexisted with scientific achievement for as long as there have been priority disputes, from the calculus to the double helix, and the science was not diminished by them. Solved problems are not dead ends. A proof of blow-up with smooth forcing poses the unforced problem more sharply; it asks whether the mechanism is stable or a measure-zero curiosity, what the singularity looks like at the scale where the continuum model fails, and whether the same iterative instability scheme reaches other supercritical equations. Each of those is a question a student can be given. Fefferman's reaction was delight, not mourning, and Córdoba and Martínez-Zoroa's ideas have been vindicated and amplified rather than buried. Even the objection about answers without understanding weakens when the mechanism is legible, as here: Tao explained the Alpöge–Buckmaster construction in a blog post within days, and OpenAI's paper at least states its strategy in terms a specialist can follow.

Something survives that reply. The ecosystem argument does not claim that mathematics stops; it claims that a particular kind of value, the slow maturation of ideas across a community and the apprenticeship of people in that process, is not captured in the theorem and can be destroyed by the speed at which the theorem arrives. This week is a test case. OpenAI's stated trigger was a rumour that a competitor had solved two Millennium problems; it then spent 88 hours confirming that its own system could do likewise. That is a competitive dynamic, and no norm among mathematicians can restrain it. Buckmaster and Alpöge did the slow year of thought, chose an unfashionable route, and were then, on their account, overtaken by the very tool they had been thinking with. If that becomes the ordinary experience of doing mathematics at the frontier, Duminil-Copin's question of what a doctoral student should now work on stops being rhetorical.

Buckmaster's own assessment is the one to sit with. He writes that "the results are not the important thing. Rather the important thing is instead the significance that a mathematician and an LLM model can now do all this work in a month", and calls it "a Deep Blue–Kasparov moment" after which "the community needs to have serious and unhurried discussion about where to go from here". The comparison holds in one further respect. After Deep Blue, chess did not end, but it changed what a human chess player is for.

What this means for society

Some consequences are institutional. Dated public disclosure is an important part of establishing mathematical priority, but it does not by itself settle questions about the origins of a proof or access to another group's unpublished ideas. It has no answer to a situation in which one party's working notes may have shaped the other party's tool, and no answer to the allegation that a co-author's name was to be dropped because of his employer. The Clay rules were written for refereed journals and a two-year settling period; they have discretion built in, but it has never been exercised on a machine-generated proof of this length.

The epistemic consequence is subtler. Formal verification, which a year ago looked like the solution to trust in machine mathematics, now looks like a large part of one. Lean can certify that a proof is valid from stated axioms, and the disclosures in OpenAI's repository show what a responsible release of such a certificate looks like. Establishing that the formal theorem matches the intended mathematical problem requires a separate semantic assessment; kernel acceptance alone does not supply it. For the wider public the lesson is sharper still: "solved", "resolved" and "proved" are now doing different work in different mouths, and a reader who does not know that Fefferman's statement has four alternatives cannot tell what has happened.

Then there is the question of who decides. A handful of companies now choose which of humanity's open problems to attack, when, and whether to say what did not work. Tao has complained that companies "rarely reveal all the things their models tried that didn't work"; OpenAI's post gives token counts but not what failed, and neither the summit that Michael Harris reports it held with selected mathematicians in early August nor the content of the rumour that reached it on 1 September has been described. Meanwhile Javier Gómez-Serrano's group at Brown, working with Google DeepMind on physics-informed neural networks to find unstable self-similar singularities, said only two weeks ago that it did not expect definitive answers "overnight" and that a candidate singularity would still need years of proof. That programme was aimed at the unforced problem. It is now the more interesting one.

Where things stand

The word "solved" is being used to cover five different things. Two groups have announced proofs: OpenAI for forced Navier–Stokes breakdown and unforced Euler breakdown, Alpöge and Buckmaster for forced Euler, Boussinesq and porous-medium breakdown. Both groups report formal checking in Lean, and OpenAI has published metadata reporting a complete formalisation using the stated standard axioms, against an adaptation of a third-party reference statement, with tools for others to re-check it. Independent assessment has several parts: rebuilding the formalisations, checking their axiom footprint, confirming that the Navier–Stokes statements match Fefferman's conditions, and assessing the human-readable arguments. The sources checked for this article do not document completion of that whole process. Mathematical understanding, in Tao's sense, is partly in hand for the Alpöge–Buckmaster mechanism, which he has already digested in outline, and largely not in hand for OpenAI's construction. Institutional recognition from the Clay Institute is governed by rules that require publication, a two-year interval and general acceptance, and OpenAI has said it will not seek it.

These five will not converge on any timetable that can be predicted from here, and the gaps between them are the story. The unforced Navier–Stokes problem remains open. The provenance question remains unresolved by the public evidence; access to adequate internal records could help answer it. What can be said with confidence is that two groups, by different routes, have announced proofs and report formal checking of claims that the Navier–Stokes and Euler equations, as posed, can develop singularities under smooth forcing; that one of them claims the same for unforced Euler; and that the manner of the second group's arrival has forced questions about credit, provenance and the purpose of mathematical work that the field had been able to postpone, until Monday night.