On 8 September 2026 OpenAI published a 166-page proof that the Navier–Stokes equations can break down in finite time, produced by about 10,000 agents over 88 hours and checked in the Lean proof assistant. Four weeks later it released 719 more manuscripts on open problems. A day after that, it withdrew three of them over a sign error. Read together, these are the clearest evidence yet of the rule this tree keeps arriving at: AI output scales exactly as far as you can verify it — and the hardest part to verify is not the answer, but whether you asked the right question.
The order matters, because the priority question turns on it.
| Date (2026) | Event |
|---|---|
| 15 Aug | Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic) obtain forced blow-up for the Euler equations, working with AI tools including OpenAI's Codex; Lean-verified about a week later, per their account. |
| 1 Sep | OpenAI starts its multi-agent run on Navier–Stokes. |
| 8 Sep | OpenAI publishes Finite Time Blowup for Navier–Stokes (166 pages) with a Lean formalisation. Buckmaster had published a statement alleging his work reached OpenAI the night before. |
| 11 Sep | Fields Medallists publish an open letter, A Severe Misalignment of AI in Mathematics. |
| 21 Sep | An independent Advisory Group on Mathematics and AI, hosted at the Institute for Advanced Study, is announced. |
| 29 Sep | The group publishes guidelines for releasing AI-generated mathematics (§05). |
| 6 Oct | OpenAI releases openai/math: 719 manuscripts in 372 families, ~42% of headline results formalised in Lean. |
| 7 Oct | Three manuscripts withdrawn over a sign error; 14 others repaired. |
The paper's Theorem 1.1: for every viscosity, there is a 3D incompressible flow that starts from rest, is pushed by a smooth force confined in space and time, keeps its kinetic energy bounded, and still develops unbounded velocity in finite time. The mechanism is a collapsing vortex whose core spins up, with carefully tuned oscillating pulses that keep the required force smooth even as the flow itself blows up.
Charles Fefferman's official Clay problem statement allows four outcomes, and proving any one wins: smoothness for ever in all space (A) or on a periodic box (B), or breakdown in all space (C) or on a periodic box (D). The paper claims (C) and (D). The breakdown alternatives explicitly allow a smooth external force, so a correct proof would settle the prize problem — Fefferman himself told Quanta he was “thrilled that the problem was solved.”
What it does not show is the version most people picture: a fluid left alone, with no force, going singular. That question stays open.
As of 11 October 2026 the Clay Institute's page lists the problem as Active and has credited no one. Clay's rules require publication in a refereed journal and two years of general acceptance before any award. There is no peer-reviewed publication yet, and OpenAI has said it will not claim the prize. Say “claimed” and “formalised”; don't say “solved” until the community does.
An unreleased internal model ran about 10,000 agents exchanging roughly 5 million messages. A second model then took 17 hours to formalise the result in Lean. OpenAI's Sébastien Bubeck put the compute cost at several million dollars (as reported by Quanta).
The same unreleased model was posed about 4,000 open problems at roughly three hours of ChatGPT Pro-level thinking each. Filtering for significance left 719 manuscripts in 372 families across many fields, including the quasi-Riemann hypothesis and cases of the Hodge conjecture.
Abridged reasoning summaries for 10 results; the model is unnamed and unavailable. The README says some unformalised results “could have issues” and corrections will ship as new versions.
This is test-time compute at its limit: enormous parallel search, made useful only because maths has a near-perfect verifier. Without Lean, 10,000 agents would have produced 10,000 plausible drafts.
Lean is a proof assistant: a small trusted kernel checks every step of a formal proof mechanically. If the kernel accepts it, the formal statement follows from the axioms — no reviewer fatigue, no skipped cases. That is why the Navier–Stokes claim was taken seriously within days rather than years.
But Lean checks the proof of the statement you wrote down. Whether that formal statement actually says what the paper claims — the right function spaces, the right hypotheses on the force, no accidentally easier variant — is a human judgement. OpenAI ships Comparator challenges for exactly this, and its own notes are careful: several comparisons “verify supporting results, not the corresponding papers' main theorems.”
One day after release, a sign error in Algebraicity of Weil classes on split abelian eightfolds invalidated it and two papers built on it; 14 more were repaired. Only about 42% of headline results were formalised at release. Unverified AI output fails the way unverified human output does — it just arrives faster and in bulk. The correction log is a credit to the release process, and a warning about reading the other 58%.
A verified answer to the wrong question is still wrong. That's the same gap spec-driven development names for code — tests that pass against the wrong requirement — and that a PhotoCraft-style corpus oracle can't catch either. Machines can now check the how. People still own the what.
Buckmaster says news of his and Alpöge's unpublished Euler work reached OpenAI and may have shaped its effort; he also asked whether OpenAI had seen his Codex sessions. OpenAI denies using the work, says the methods differ significantly, and has said Buckmaster's prompts could not have influenced the result — though its public wording on that point shifted several times over the following week. None of it is resolved, and both sides' accounts of private conversations differ.
Whatever the facts, the structural point stands: when your research runs on a vendor's model, the vendor is also a competitor for the result. That's a governance question for any business, not just mathematicians — see the briefing Your Prompts Are R&D.
The openai/math release meets some of these (versioned corrections, partial formalisation, some reasoning summaries) and not others (the model is unnamed, and there's no failure report).
The transferable rule: buy generation in bulk only where you own a strong checker — and keep a person on the statement of the problem.
| Domain | The verifier | How far you can scale |
|---|---|---|
| Formal maths | Lean kernel | Very far on proofs; a human still checks every formal statement. |
| Software | Types, tests, CI gates | Far — as far as your tests encode the real requirement. |
| Tax & accounting rules | Golden tests, cited law | Moderate: checks coherence, not legal correctness; needs a practitioner sign-off. |
| Contracts, strategy, advice | None automatic | Barely: every output needs expert review, so bulk generation just moves the bottleneck. |
SA mathematics departments and research teams have no access to unreleased frontier models or million-dollar compute runs — precisely the two-tier system the advisory group warns about. The accessible parts of this story are the open ones: Lean and its mathlib library are free, the openai/math artefacts are Apache-2.0, and checking or formalising published results is work a small team can do on a laptop. For SA businesses the lesson is the verifier: before buying AI generation in bulk, ask what checks it — and keep unpublished IP off platforms where you can't see what the vendor retains.
Figures on agents, messages and cost come from OpenAI's statements as reported by Quanta; the dispute is described from both sides' public accounts. Last reviewed 2026-10-11.