The proof no one has read: OpenAI, Navier–Stokes and the limits of verification

On 8 September OpenAI announced that an internal system, described only as significantly more capable than the model it sells as GPT-6 Astra, had constructed a solution to the three-dimensional incompressible Navier–Stokes equations which starts from rest and develops unbounded velocity in finite time. The write-up runs to 166 pages. A second model then spent seventeen hours translating it into Lean, the proof assistant, where a kernel of a few thousand lines checked every inference against the axioms and raised no objection. The files sit on GitHub, under openai/NavierStokesAndEuler, and anyone with a laptop and patience can compile them.

Buried in the company's own account is a sentence most of the coverage hurried past: OpenAI does not intend to claim the Millennium Prize. That is neither modesty nor quite a disclaimer. It is the most informative line in the announcement, and understanding why requires knowing precisely which theorem was proved — a matter on which much of the reporting that followed was simply wrong.

Three things happened in the same week, and they are separable. A mathematical statement of real interest was established. A dispute about credit broke out between OpenAI and two mathematicians working the same seam. And a question philosophers of mathematics have argued about since the 1970s stopped being a seminar exercise, because there now exists an important result certified correct by a machine and understood by nobody.

The theorem is narrower than the headline, and that narrowness is the story#

The Clay Mathematics Institute's official description of the problem was written by Charles Fefferman in 2000, and it does something unusual: it offers four statements, labelled (A) through (D), and says that proving any one of them settles the problem. (A) and (B) assert that smooth, finite-energy initial data always produce smooth solutions for all time, on R³ and on the periodic torus respectively, with the external force set identically to zero. (C) and (D) assert the opposite — that there exist smooth initial data and a smooth external force for which no such solution exists.

OpenAI's system proved (C), and with it (D). The abstract of the resulting paper is admirably plain: for every positive viscosity, it constructs a solution of the three-dimensional incompressible Navier–Stokes equations that starts from rest and develops unbounded velocity in finite time while keeping kinetic energy uniformly bounded. The mechanism is a self-similarly concentrating axisymmetric vortex — a whirl drawing itself inward and stretching out, spaghetti-like — paired with oscillatory pulses arranged so that nonlinear advection outruns viscous dissipation.

So it is an official alternative, and on the face of the rules it qualifies. But the forcing term is doing enormous work. One may pick a velocity field that blows up in a convenient way and then define the force to be whatever the equations require, so that the difficulty reduces to arranging a cancellation; in the unforced case the remainder has to vanish rather than merely be well behaved, which is categorically harder. Nick McGreivy, writing a technical explainer the week of the announcement, put the hierarchy bluntly: it is much easier to find singularities in forced fluids than in unforced fluids. Every working analyst knew this before September. It is why (A) and (B) — the question of whether a fluid left to itself can tear a hole in its own description — remain exactly as open today as they were in August, and why the phrase "AI solved Navier–Stokes" flatters the result while, in an odd way, also diminishing it.

Diminishing it, because the construction is not trivial. It sits on a programme developed by Diego Córdoba of the Institute for Mathematical Sciences in Madrid and Luis Martínez-Zoroa of CUNEF University, whose names appeared in almost none of the first-day coverage and, initially, in none of OpenAI's references — an omission the company corrected in a revised version after complaints. Charles Fefferman, asked by El País whether the formal statement was the right one, said it matches the problem as he framed it, but will need a rewrite into conventional mathematical prose and close reading by several experts, a process he expected to take months.

The numbers, and who is responsible for each of them#

OpenAI's own figures for the Navier–Stokes run: roughly 10,000 concurrent agents, 88 hours from launch to resolution, 2.7 million messages exchanged between agents, approximately 130 billion output tokens, and a further seventeen hours for formalisation and verification in Lean 4.34.0-rc2 against Mathlib. A separate, much smaller effort — about a hundred agents over some fifty hours — produced an unforced blow-up result for the Euler equations, which is a different and in some respects more striking theorem.

The money is harder. Sébastien Bubeck, the OpenAI researcher at the centre of the episode, told reporters: "We are able to spend millions of dollars on a problem that we really care for." VentureBeat did the obvious arithmetic — 130 billion output tokens at the published GPT-6 Astra rate of $50 per million — and arrived at about $6.5 million for output alone, at retail rates and excluding input. TechCrunch reported $22.5 million for the whole week-long effort across several problems, and 300 billion output tokens in total. Figures between $10 million and $40 million circulated without clear attribution. A widely repeated claim that the Washington Post costed the run at $15 million could not be confirmed from the Post's own pages, which sit behind a paywall; this article does not rely on it.

What is not in dispute is the ratio. The compute bill exceeded the prize by a factor of somewhere between six and twenty; claiming the million dollars would have been a loss-making transaction. That is one reason OpenAI declined it, and a fact worth sitting with.

A proof can be certified and still explain nothing#

Here the episode stops being a technology story. Philosophers of mathematics have long distinguished proofs that establish a theorem from proofs that show why it is true, and the distinction is neither soft nor recent.

Mark Steiner set out the sharpest version in "Mathematical Explanation", published in Philosophical Studies in 1978. An explanatory proof, on his account, turns on a characterising property — a feature that singles out the object in question within some family of objects — in such a way that the result visibly depends on that feature. His test is deformability: vary the characterising property and the proof should deform with it, yielding a family of related theorems rather than breaking. A proof that grinds out the conclusion by an exhaustive route passes no such test. Philip Kitcher's rival account, developed in "Explanatory Unification" (1981), locates explanation elsewhere: in economy of argument patterns, in deriving the largest number of results from the smallest stock of derivational moves, so that what looked like a scatter of separate facts turns out to be one fact seen from several angles. Marc Lange, in Because Without Cause (Oxford, 2017), ties it to salience — a proof explains when the feature it exploits is the feature that makes the result striking. His best example is a grid of the digits one to nine from which sixteen different numbers can be read off, all divisible by 37. You can verify all sixteen by division and learn nothing. The explanation arrives only when someone shows they are instances of a single arithmetic pattern.

The three accounts disagree about almost everything, which is a point in their favour: they disagree because there is something real they are all trying to describe. Each is orthogonal to formal verification. Lean does not check for characterising properties, argument-pattern economy or salience; it checks that the inferences are valid. That is a magnificent thing to be able to check, and it is not this thing.

Terence Tao made the same point in his 2024 essay for the Notices of the American Mathematical Society, and made it against his own interest as an enthusiast for proof assistants. Formalisation, he wrote, "provides an extremely high level of confidence that a given result is correct, which is particularly valuable for results that are controversial or notorious for attracting false proofs" — Navier–Stokes being a magnet for false proofs of exactly that kind. But he then listed the caveats, of which the sharpest is that "the definitions used in the formal statement of the result may differ in subtle but important ways from the human-readable statement." A green light from Lean certifies that the Lean statement follows. Whether the Lean statement is the Clay statement is a judgement no compiler makes, and Fefferman's estimate of months concerns precisely that.

Mathematics has been here before, on a smaller scale. The 1976 four-colour theorem depended on a case analysis too large to read; Tao records that the unavoidability computation ran to hundreds of pages of microfiche and was checked by hand by Dorothea Blostein, Wolfgang Haken's daughter, who found multiple errors, all fixable. The community absorbed it, grumbled for a decade, then stopped grumbling. But four colours was a single computation embedded in a human argument. This is 166 pages of argument.

What proofs are for, according to the people who use them#

Tao published the clearest statement of the stakes on 7 September, the day before OpenAI's announcement, in a post on the Alpöge–Buckmaster results. Discussing what makes such work valuable, he wrote that "the actual solving of these problems is only a proxy goal for the primary goal of developing mathematical understanding and insight." That is not a complaint about machines. It is a description of what the profession takes itself to be doing, offered by someone who also noted, approvingly, that the arguments in question "are heavily AI-assisted" and that the work "has also been formalized in Lean."

Tao's objection, when it came, was to a method rather than a machine. Speaking to Fortune, he warned that the indiscriminate strip-mining of open problems for solutions could destroy the ecosystem from which the next generation of mathematical techniques emerges, and likened it to using excavators to loot an archaeological site: you get the treasure and destroy the stratigraphy that would have told you what it meant. Part of the complaint is about dead ends. Mathematicians discuss their failures because a documented failure narrows the search for everyone. An agent swarm that discards 2.7 million messages and emits only the winning path throws away the map and keeps the coordinates.

Michael Harris, the Columbia number theorist whose newsletter Silicon Reckoner has tracked the mechanisation of mathematics since 2021, was less measured. On 8 September he called the episode "demeaning to mathematics" and accused the industry of "using prominent mathematicians as extras in a marketing operation masquerading as a drama." His substantive worry was about recruitment: the spectacle "convinces decision makers that human mathematicians are obsolete, and it convinces young people that their passion for mathematics has no future." One may think Harris overstates and still concede that he describes a real mechanism, because a subject that cannot recruit cannot referee, and a subject that cannot referee cannot certify anything.

Córdoba was more generous and more pointed at once: he acknowledged what the machines had done and observed that had his group's work not existed, the system would not have solved the problem. Gregory Eyink of Johns Hopkins gave Science News the sentence that will probably outlive the week: "I don't think anyone has completely verified the proof yet, certainly not on the human side." Buckmaster, who has more reason than most to be sour, called it a Deep Blue–Kasparov moment and asked for "serious and unhurried discussion about where to go from here."

Searle's question, asked properly, and Gödel's, dismissed briefly#

The temptation is to reach for the Chinese Room and stop. Searle's argument was that a system manipulating symbols by rule, however fluently, has syntax without semantics — it does not understand the Chinese it emits. Applied here, the argument has an awkward consequence that is rarely noticed. The Lean kernel is a Chinese Room in the strictest sense: a few thousand lines of code applying inference rules to strings, with no access whatever to what fluids are. And the mathematical community trusts it more than it trusts any human referee. Searle's conclusion is correct about the kernel and beside the point, because nobody asked the kernel to understand. The live question is whether the searcher does; and the honest answer is that the swarm exhibits some of what we would count as understanding in a person — it transfers techniques across domains, recognises when an approach is exhausted, reformulates — and none of what we would count as understanding in a mathematician, since it produced no account of why the vortex construction works that anyone has been able to lift out and teach. Dennett's functionalist reply and Chalmers on organisational invariance are live options here; what neither supplies is the missing item, which is not consciousness but exposition.

Gödel deserves a shorter hearing. The Lucas–Penrose argument holds that because a human mathematician can see the truth of the Gödel sentence of any consistent formal system, human mathematical insight cannot be captured by such a system. The refutations are well established — Solomon Feferman's review of Shadows of the Mind, Stewart Shapiro's "Mechanism, Truth, and Penrose's New Argument", Peter Koellner's two-part analysis — and they turn on the point that the mathematician sees that truth only conditionally, on an assumption of consistency which is precisely what is not available. In any case the argument is idle here. OpenAI is not claiming its system transcends formal systems; it claims the opposite, that everything it produced reduces to inferences a formal system verifies. Whatever is troubling in that, it is not incompleteness.

The dispute over credit, reported as carefully as it deserves#

The chronology, reconstructed from OpenAI's statements, Buckmaster's public posts and contemporaneous reporting, runs as follows. Levent Alpöge, a researcher at Anthropic, and Tristan Buckmaster of New York University had collaborated privately for about a year on the Córdoba–Martínez-Zoroa programme, using models from both Anthropic and OpenAI, including Codex. They obtained forced blow-up results for the Euler, incompressible porous medium and Boussinesq equations on 15 August and had them verified in Lean by 22 August. OpenAI began training the relevant model on 28 August and on 1 September launched a large run across the open Millennium problems, after hearing rumours that Anthropic researchers had solved one. On 6 September Bubeck informed both men that OpenAI had a Navier–Stokes result. Buckmaster posted his and Alpöge's results shortly before midnight on 7 September; OpenAI announced twelve hours later.

Buckmaster's allegation has two parts, and they should not be run together. The first concerns data: he used Codex heavily, uploaded unpublished drafts into private sessions, and observed that OpenAI's agents had pursued the one obscure approach he and Alpöge were pursuing. His own words were careful — "I do not know whether our data was used. I am not accusing anyone of anything." OpenAI's chief research officer Mark Chen said that "no people or AI systems searched through user data to solve this problem or any specific problem," and the company later stated categorically, after an internal investigation, that Buckmaster's Codex prompts over the preceding two months could not have influenced the system in any way, including through training. It conceded in the same breath that "while unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models" — a narrower admission, and not nothing.

The second part concerns conduct. Buckmaster says Bubeck proposed, as a compromise, that Alpöge's name be left off a joint write-up because of his Anthropic affiliation, and that when he refused the conversation turned unpleasant. Bubeck has denied the characterisation and apologised for his choice of words at the meeting. Buckmaster has said publicly that the prize money was never his concern and that the removal of Alpöge from authorship was "the big sticking point." OpenAI proposed that the two men receive the Clay prize as the humans closest to the problem; Buckmaster declined. These are contested recollections of private conversations, and this article records them as such.

On 11 September the Clay Mathematics Institute issued a statement notable for saying nothing about anyone. It shares "in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled," notes that its rules govern the evaluation of what has been achieved and the assignment of credit, and adds that "the process is deliberately unhurried." Those rules require publication in a qualifying outlet, two years elapsed since publication, and general acceptance in the global mathematics community. The Institute expressed the hope that "waves of new human understanding" would follow as the innovations are analysed and interrogated. Read closely, that is a condition, not a pleasantry.

Compute as a condition of discovery#

The economics have consequences that survive whatever one concludes about the mathematics. A result of this kind now requires resources held by perhaps five organisations on earth, none of them universities. Joachim Escher of Leibniz University Hannover made the arithmetical point that one cannot put every mathematical problem to such a system, because the energy and capacity do not exist; Abhishek Saha of Queen Mary University of London added that very few problems are prestigious enough to justify the outlay. The result is a strange selection effect. Famous problems will be attacked by machines that do not explain themselves, and merely important ones left to people — close to the inverse of how a healthy discipline allocates attention.

There is a second consequence, for norms. Mathematical credit has been governed for three centuries by an informal system of priority, citation and refereeing that works because the participants are few, known to each other and repeatedly interacting. A corporate laboratory publishing by press release, as Tao has objected, enters that system without being subject to its sanctions. Zsuzsanna Dancso of the University of Sydney reduced the complaint to two rules: acknowledge your sources, and acknowledge your collaborators. The first was breached, then repaired; the second remains disputed.

Whether the community will accept what it cannot read#

The question now facing mathematicians is unusually concrete, and their answer will be a statement about what proof has been for. A Lean certificate is available today. A human-readable account is months away at best, and may never be produced in a form that transmits insight, because the argument was not built by anyone trying to transmit anything. If the community accepts the result on the certificate alone, it will have decided that proof is fundamentally a guarantee of correctness, and that explanation is a pedagogical extra. If it withholds acceptance until someone can stand at a blackboard and say why the vortex tears, it will have decided that a proof is a communicative act and that an uncommunicated one is incomplete, however sound.

Neither answer is obviously right. The first has the better claim to what proof formally is; the second has the better claim to what mathematicians have actually done with proofs, which is to mine them for techniques and hand them to students as instruments rather than conclusions. Tao's formulation — that solving is a proxy goal for understanding — is a hypothesis about the profession's purposes, and the profession is about to test it under conditions it did not choose.

What can be said with confidence is smaller than the headlines and more interesting. The unforced problem, the one that has drawn a century of effort, is untouched. A machine has settled a real alternative in Fefferman's formulation and produced a certificate no human has audited. And Clay, in the driest available language, has made its prize contingent on something no compiler can deliver.