TL;DR
- OpenAI says an unreleased internal model and roughly 10,000 coordinated agents produced a proof that smooth Navier–Stokes fluid motion can develop a finite-time singularity.
- The company has published a written proof and Lean formalisation, but the Clay Mathematics Institute still lists the problem as unsolved and formal recognition requires years of independent scrutiny.
- OpenAI reports 88 hours of agent work, 2.7 million messages and about 130 billion output tokens, followed by 17 hours of Lean work with GPT‑6 Astra.
- A priority and data-provenance dispute with Tristan Buckmaster and Levent Alpöge remains unresolved; both their claims and OpenAI’s response need attribution.
In plain English
Navier–Stokes equations describe how fluids such as air and water move. The Millennium problem asks whether smooth starting conditions can ever produce a mathematical breakdown in three dimensions.
A singularity, or blow-up, is a point where the equations make a quantity such as fluid speed grow without bound in finite time.
A formalisation in Lean expresses the argument in a form that software can check step by step. It strengthens error checking, but mathematicians still need to assess the statement, assumptions and significance of the result.
A multi-agent system divides work among many AI instances. In this case, groups explored different variants, exchanged findings and had useful ideas consolidated into later rounds.
OpenAI says an internal AI system has resolved the Navier–Stokes existence and smoothness problem, one of mathematics’ seven Millennium Prize Problems. The company has released a written proof and a formalisation in the Lean proof assistant. Its claim is that smooth three-dimensional fluid motion can develop a singularity in finite time.
That is an extraordinary result if it survives mathematical review. It is also a useful demonstration of what large-scale agent systems now look like: an unreleased model, thousands of agents working in groups, millions of messages, code and internet tools, consolidation by Codex, and a separate formal verification stage.
The first distinction to keep clear is between a published claim and an accepted solution. The Clay Mathematics Institute still lists Navier–Stokes as unsolved. Its prize rules require a proposed solution to appear in a qualifying outlet, remain published for at least two years and receive general acceptance from the global mathematics community before the institute will consider it. OpenAI says it does not intend to claim the prize.
The problem asks whether the Navier–Stokes equations, which describe fluid motion, always produce smooth behaviour from smooth starting conditions in three dimensions. The equations are central to modelling air, water and other fluids. A singularity would mean a quantity such as fluid speed becomes unbounded in finite time, marking a breakdown in the mathematical model.
OpenAI says it began the effort on 1 September after hearing rumours that two Millennium problems had been resolved. It asked groups of agents to try all four official variants of the Navier–Stokes problem, along with several related problems.
The successful Navier–Stokes group involved on the order of 10,000 concurrent agents. They could use code and a cached version of the internet, communicate within groups and explore different approaches. OpenAI used Codex to consolidate promising ideas between groups and moved more agents onto Navier–Stokes after a smaller group found a related result for the Euler equations.
According to the company, the Navier–Stokes agents reached their result after about 88 hours. They exchanged 2.7 million messages and generated roughly 130 billion output tokens. GPT‑6 Astra then took another 17 hours for Lean formalisation and verification. The unreleased model that ran the agent groups remains internal, is still being trained, and OpenAI describes it as significantly more capable than Astra. It is distinct from Codex, which handled consolidation between groups.
The system was organised as a temporary research operation: many workers tried variants in parallel, results were shared and consolidated, resources were redirected towards the most promising route, and a second system checked the output. It is a concrete example of capability emerging from orchestration and scale as well as from the underlying model.
It is not yet a reproducible account of that capability. Outside researchers do not have access to the internal model or the complete agent environment, and OpenAI has not attached a compute cost to the run. The proof can be examined, but the research system which generated it cannot currently be rerun independently.
There is also a dispute about how the project began and who deserves credit for the route it took. Mathematicians Tristan Buckmaster and Levent Alpöge had been working on related Euler and Navier–Stokes questions with assistance from several AI systems. Buckmaster says OpenAI began its push after learning of their progress and questions how its system arrived so quickly at a similar forcing-based direction. He has said he does not know whether their data was used.
OpenAI says neither its researchers nor its agents saw Buckmaster and Alpöge’s work before it became public, and that no specific user data was accessed to solve the problem. It also says it cannot rule out the possibility that de-identified product usage contributed to model training. The company recognises Buckmaster and Alpöge’s priority on their forced-Euler result while saying the proofs and precise results differ.
Independent reporting from Scientific American describes mathematicians reacting with surprise and caution while the community compares the approaches. The appropriate conclusion for now is not that the dispute has been settled, but that scientific credit, training-data provenance and AI-assisted discovery have collided in one unusually visible case.
For people building agent systems, the immediate lesson is not that every hard problem yields to 10,000 workers. It is that frontier capability may increasingly depend on the surrounding research machinery: how tasks are divided, how agents communicate, when partial findings are consolidated, which tools they can use and how results are checked.
For everyone else, the status is simpler. OpenAI has made a specific, inspectable mathematical claim and disclosed striking operational figures for how it was produced. The proof now has to earn acceptance through the slower process that a result of this importance requires.