OpenAI's Navier–Stokes proof: what 10,000 AI agents actually changed

On 8 September 2026, OpenAI said an internal AI system had produced a written proof and a Lean formalisation showing that the forced, three-dimensional Navier–Stokes equations — a 90-year-old open question about whether smooth fluid motion can break down — can develop a singularity in finite time. That is one of the seven Millennium Prize Problems the Clay Mathematics Institute set in 2000, each carrying a $1 million prize. The headline is the maths. The more useful story, for anyone trying to understand where AI research is actually heading, is the machine that produced it: how many agents, how long they ran, what they cost, and how a rival human-and-AI team got a related result first with a fraction of the resources.

OpenAI's own framing is precise about scope. The claim is that a fluid starting smoothly at rest, subjected to a smooth applied force with finite energy throughout, develops a singularity — a point where speed grows without bound — in a finite amount of time. That satisfies what the Clay Institute's official problem statement calls options C and D: variants of the question in which a disproof (rather than a proof of universal smoothness) counts as a resolution. The solution, OpenAI says, is a vortex that spirals inward and stretches, its rotational speed increasing as its core shrinks, while its total energy — as physics requires — stays finite throughout.

That model, still in training and still improving by OpenAI's own account, is what makes the timeline plausible at all. The company says it heard rumours on 1 September that two mathematicians had resolved a related Millennium Problem, and used that as the trigger to point its new model at all six then-unsolved problems simultaneously, plus a set of adjacent, easier questions.

The mechanics are the real news for anyone assessing where AI-for-research spending is going. OpenAI ran groups of coordinating agents against different framings of each problem, let different groups explore different approaches, and periodically used its Codex system to cross-pollinate the most useful intermediate results between groups. One easier variant — blow-up in the unforced Euler equations, a simplified relative of Navier–Stokes with viscosity removed — fell first, and fell cheaply.

That precursor result reset OpenAI's priorities: having seen the Euler answer, the company decided Navier–Stokes was the most tractable of the remaining problems and reassigned agents accordingly, feeding them the Euler solution as a starting point. The group that eventually found the Navier–Stokes resolution scaled to roughly 10,000 concurrent agents, reached its answer after 88 hours, and needed a further 17 hours for a separate model to formalise and check the proof in Lean — the automated proof assistant that rejects any step that does not follow rigorously from the axioms before it. Across every problem the agents attempted, OpenAI counted almost 4.9 million inter-agent messages; roughly 2.7 million of those belonged to the Navier–Stokes effort alone.

OpenAI was not alone, and was arguably not first. Roughly 12 hours before OpenAI's announcement, NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge published their own Lean-verified proof — for the forced Euler equations, a related but distinct result — using a mix of models including Anthropic's Claude and OpenAI's own Codex and Astra. Both efforts leaned on the same underlying mathematics: a technique for building an infinite 'cascade' of non-singular solutions that Diego Córdoba and his former doctoral student Luis Martínez-Zoroa developed analytically, without computer assistance, starting with Martínez-Zoroa's 2021 dissertation and a joint 2023 paper. OpenAI has publicly ceded priority on the forced Euler result to Buckmaster and Alpöge while claiming the larger Navier–Stokes result for itself.

The durable change is procedural, not mathematical. A frontier lab can now point an unreleased model and a five-figure agent swarm at a named, famous, unsolved problem and get a formally checked candidate answer within days — as long as a human-built technique exists for the agents to extend. That is a genuinely new mode of research production: not a model that invents an approach from nothing, but one that can rapidly explore, combine and formalise variations on an approach a human mathematician has already opened up. Córdoba and Martínez-Zoroa did the hard conceptual work over several years without AI; two different AI-assisted teams then raced to close the last, formalisable gap in about a week.

Formal recognition is a separate, much slower track. OpenAI has said explicitly it will not claim the Clay Institute's prize money, and the Institute's own rules require publication in a recognised venue, a minimum two-year wait, and broad acceptance by the mathematical community before any Millennium Problem is declared solved — a bar only the Poincaré Conjecture has ever cleared. Worth watching in parallel: whether the unforced version of Navier–Stokes, which most mathematicians consider the scientifically meaningful question, turns out to be reachable by the same cascade technique at all — a September 17 preprint from three mathematicians argues it structurally cannot be, at least not this way.