OpenAI's Navier-Stokes Proof: What Was Claimed, Who Checked It, Who Gets the Credit

What OpenAI claimed

On 8 September 2026 OpenAI posted 'On the Navier-Stokes Millennium Prize Problem', saying an internal system had produced an analytical proof and a Lean formalisation that an initially smooth fluid at rest, with a smooth force applied, can develop a singularity in finite time while its energy stays finite. OpenAI says this 'resolves the Navier-Stokes Millennium Prize problem by establishing statement C (and also D)' in the official formulation, and also that 'we do not intend to claim the Millennium Prize for this result'. The model is described as an internal one 'significantly more capable than GPT-6 Astra', in training since 28 August.^[S1]

The paper, 'Finite time blowup for Navier-Stokes', runs to 166 pages and is signed only 'OpenAI'. Theorem 1.1: for every ν > 0 there is a force f, smooth and compactly supported in space and time, and smooth velocity and pressure on [0, 1) with u(·, 0) = 0, uniformly bounded kinetic energy, and the limsup of the velocity's L∞ norm infinite as t approaches 1. The paper says this establishes alternative (C) in Fefferman's statement, and that compact support gives (D) on the torus T³ (Corollary 10.6).^[S2]

Clay's official statement does admit a force: (C) asks for a smooth divergence-free initial field u° and a smooth force f, both meeting decay conditions, for which no solution with the stated smoothness and bounded energy exists. So the forcing is not outside the letter of the problem. The unforced question (whether smooth solutions exist for all time with no force) is still open, and the force here is built to sustain the collapse.^[S7][S16]

How it was found, on OpenAI's account

On OpenAI's account: after hearing on Tuesday 1 September a rumour that two Millennium problems had been resolved, it set a system of coordinating agents, powered by the internal model, on every open Millennium problem, giving separate groups variants A/B (the proof direction) and C/D (the disproof direction). Agents could read a cached copy of the internet and run code. Among a set of 'easier' problems, nearly 100 agents working about 50 hours resolved unforced Euler blowup; OpenAI then moved its resources to Navier-Stokes, prompted agents with the Euler resolution, and used Codex to pool the groups' intermediate results and feed them back. The group that solved Navier-Stokes had on the order of 10,000 concurrent agents and arrived on Saturday 5 September, about 88 hours after launch; Lean formalisation and verification took another 17 hours via GPT-6 Astra. Across all problems the agents sent 4.9 million messages and used about 300 billion output tokens; Navier-Stokes alone took 2.7 million messages and about 130 billion.^[S1]

All of this is OpenAI's own statement; no logs are public to check it against. Buckmaster's statement says he was told the model had simply been given the problem statement, and Alpöge had been told by Bubeck that 'very little human input' had been used; corrections from OpenAI's team during the call then showed that a whole team had worked on it, that work began on the unforced problem and easier problems including Euler, and that the prompt he was shown had itself been written by prompting Codex.^[S1][S10]

Which sentence the machine checked

OpenAI's Lean repository (Lean 4.34.0-rc2 with Mathlib, Apache-2.0) does not write its own problem statement. It adapts the Navier-Stokes encoding that already existed in Google DeepMind's Formal Conjectures project, and ships Comparator challenge files so anyone can check that the proved theorem's type matches the reference statement. We diffed OpenAI's NavierStokes/ComparatorDefinitions.lean against formal-conjectures at commit 8bf45ed: the changes are the import, the namespace, notation made local, category attributes stripped, the module docstring rewritten, and the four sorry placeholders for (A)-(D) removed. No structure definition changes mathematically, and the (C) statement in ComparatorSolution.lean is character-for-character the one the upstream file left to be proved.^[S4][S5]

That is what is new here: the question 'is this the problem that was asked' no longer has to be settled by reading 166 pages; one diff shows that the proved statement matches a formal statement written in advance. But a diff does not by itself complete the whole semantic check: whether that formal statement gets every requirement of Clay's (C) right is still a matter of people reading it. And what the machine check establishes holds relative to that formal statement, Lean's axioms and its trusted kernel. Whether the prose paper is correct, or readable, is yet another question.

Credit: three accounts

By 7 September, when Tao wrote about them, Buckmaster (NYU) and Alpöge (an Anthropic employee, working in a personal capacity) had made public three finite-time blowup results with smooth forcing (incompressible porous media, Boussinesq and 3D incompressible Euler), with Lean formalisations. Buckmaster credits the basic idea of the programme to years of forced-blowup constructions by Córdoba and Martínez-Zoroa, and says he and Alpöge pushed it to smooth forcing and to Euler with a great deal of help from LLMs; the tools he lists are Anthropic's Claude and OpenAI's Codex, with GPT-5.6 Sol and more recently Astra. Tao's 7 September post likewise attributes the strategy to Córdoba and Martínez-Zoroa, and says the Alpöge-Buckmaster variant has 'a high likelihood' of extending to Navier-Stokes.^[S10][S11]

OpenAI's paper cites Córdoba, Martínez-Zoroa (and Zheng) as having established a strategy of singularity formation by amplification across scales, and says its own construction also uses dynamical amplification but gives the amplified disturbances a different role; the paper does not mention Alpöge or Buckmaster. OpenAI's post 'recognize[s] the priority of their work on forced Euler' and stresses that the two Euler results differ: theirs forced, OpenAI's unforced. Credit for Navier-Stokes itself OpenAI assigns to no one else.^[S2][S1]

Buckmaster writes that 'forced' was 'a bright red flag' to him: the route to the Clay problem through a smooth force, options c and d in Fefferman's statement, is the one Córdoba and Martínez-Zoroa opened and he and Alpöge had quietly chosen, 'almost nobody else' was on it, and it is not where a model given the problem statement arrives in a few days. He says OpenAI eventually agreed its first prompt had been sent in the past few days, 'after information about our work had reached OpenAI', and that when he asked whether the model had been trained on the drafts they put into Codex, he got no answer. He also writes that he has not seen OpenAI's proof, does not know what the model did or whether their data was used, and is 'not accusing anyone of anything'.^[S10]

OpenAI's answer exists in two versions of its post. TechCrunch (8 September) and The Next Web (10 September) quote it as: 'While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models.' The version we read on 26 September says instead: 'Following an investigation, we have confirmed that Buckmaster's Codex prompts over the two months preceding this announcement ... could not have influenced the system in any way, including through training.' The page does not mark the change, and neither the investigation's method nor its material is public.^{[S12][S13][S1]}

Authorship is two accounts as well. Buckmaster says Bubeck twice said on the 6 September calls that he wanted Alpöge removed from authorship, and answered his plan to go public with 'Why would you ruin your career?'. Bubeck, in posts on X relayed by The Next Web, denies ever asking to remove Alpöge from authorship of his own work, says his remark that 'it would be simpler if Levent was not an Anthropic employee' concerned a proposal for the pair to co-write OpenAI's proof, and apologises for the career remark. These are opposing accounts of private calls, and no independent process has tested them.^[S10][S13]

Who has checked what

These are really four different questions with evidence of different strength: whether the machine check passes; whether the formal statement corresponds to Clay's; whether the natural-language argument has been reviewed; and how priority and the prize are assessed. Code can answer part of the first two; the last two need people and process. What follows takes them in that order.

OpenAI itself.

The repository's formalization.yaml records a sorry count of 0, main theorems depending only on Lean's three standard axioms (propext, Classical.choice, Quot.sound), the formalisation done by GPT-6 Astra through Codex, and a review status of 'self-assessed'.^[S4]

One outside GitHub account.

CrystalArchitect/navier-stokes-lean-check reports a build from source on macOS, 11,251 jobs successful, and axiom lists for both main theorems with no sorryAx; the definitions are byte-identical to formal-conjectures. It also says it did not run the independent nanoda kernel replay (Comparator's landrun is Linux-only) and that whether the prose paper is correct is out of its scope. Who runs the account is not stated. We read its README; we did not build the Lean project ourselves, and the statement diff above is our own.^[S6]

Mathematicians: building on it is not refereeing it.

A preprint by Constantin, Ignatova and Vicol (17 September) proves that solutions with two key features of the construction (an angular mean obeying specific anisotropic Type II bounds, and exact axisymmetry in a collapsing core region) are in fact regular at the putative singular point when the force is real-analytic in space. Its abstract concludes that in OpenAI's construction, and in any construction with those two features whose force stays bounded in C² up to the singular time, the force can neither vanish identically near the singular point nor be real-analytic in the space variables, locally uniformly in time. What is ruled out is the force being identically zero on a neighbourhood of the singular point, not the force taking the value zero at that point. That bounds the result; it is not a referee report on its correctness. Other preprints take OpenAI's construction as given and derive density results from it. Tapio Schneider, in a guest post on Tao's blog (23 September), writes that the formal verification supports correctness but mathematicians are still working to digest it.^{[S14][S15][S16]}

The Clay Institute: not yet.

Clay's 11 September statement says it shares the excitement at the announcement that the Navier-Stokes problem 'has apparently been settled', and that its rules set the process for evaluating what has been achieved and assigning credit, a process that is 'deliberately unhurried'. Those rules require publication in a qualifying outlet, at least two years since that publication, general acceptance in the global mathematics community, and then Clay's own judgment that the official questions were answered; Clay does not accept submissions directly. OpenAI's paper is so far only on its own site, and OpenAI says it will not claim the prize.^[S8][S9]

Why this is rung 2

The proof is a result that exists in software and text: a paper and a Lean project that compiles. On this site's ladder a proof sits at 'computed'; the machine check makes that rung firmer but does not move it to 'checked against existing evidence'. That the Lean statement was written in advance by a third party is an unusual strength; as far as we could find by 26 September, the only public assessment of the prose argument is its authors'.

Three things to record separately

Who claimed: OpenAI, as a company, with no named authors. Who checked: the Lean kernel (self-assessed by OpenAI, plus one outside rebuild by an unidentified account), against a formal statement written in advance; as of 26 September no public independent referee report on the prose was found. Who is credited: OpenAI credits Navier-Stokes to no one else and recognises Alpöge and Buckmaster's priority only on forced Euler; Buckmaster credits the whole route to Córdoba and Martínez-Zoroa; Clay's process has not begun. Writing all three as 'AI solved a Millennium problem' collapses three kinds of evidence of very different strength into one.

Formalisation separates 'is it right' from 'is it the question asked'

For a major proof claim the harder check has often been the second: whether the theorem quietly says less than the announcement. Borrowing a statement a third party wrote beforehand lets a diff rule that out. It cannot rule out a provenance question, because provenance is a claim about a training and interaction process no outsider can inspect.

Scale has become a property of the instrument

About 10,000 concurrent agents, 88 hours, about 130 billion output tokens: few organisations could repeat that search at the same scale. What anyone can reproduce is the Lean check; what no one outside can reproduce is the process that produced the proof.^[S1]

External oversight is forming, without authority

On 21 September nine mathematicians announced the Advisory Group on Mathematics and Artificial Intelligence, hosted at the Institute for Advanced Study. It began when OpenAI approached some members about an external advisory board and they agreed instead to form an independent group. Its current task is advising OpenAI on coordinating the release of 'a large number of significant results in mathematics' its internal model reportedly produced; members are unpaid, and the group has no decision-making power at any AI company. Member Martin Hairer wrote in a follow-up guest post that the publication of high-profile mathematical results by AI companies in recent months has fallen 'far short of acceptable mathematical practice'.^[S17][S18]