OpenAI says 10,000 agents spent 88 hours on two Navier-Stokes clauses
An unreleased model used about 130 billion tokens, a bill OpenAI priced at roughly $10 million. The company published a Lean file, says it will not claim the Clay $1 million prize, and has offered its prompts to two mathematicians already working the problem.

San Francisco3 min read
Last updated
OpenAI said on Tuesday that an unreleased model, running through about 10,000 largely autonomous agents, produced a solution to two of the four statements in the Navier-Stokes existence and smoothness problem after 88 hours of work.
The Clay Mathematics Institute listed that problem in 2000 as one of seven Millennium Prize Problems, each carrying a $1 million award. The equations, written in the nineteenth century by Claude-Louis Navier and George Stokes, describe how viscous fluids move. Mathematicians have never proved that smooth solutions always exist in three dimensions, or that they stay smooth rather than blowing up into singularities. Those two questions sit at the centre of turbulence, a phenomenon that weather models and aircraft design still treat with approximations.
OpenAI said the agents exchanged nearly 3 million messages and used about 130 billion output tokens on this task alone. At the company's published prices for its most capable models, that volume of output would cost around $10 million. A separate model, GPT-6 Astra, then spent about 17 hours checking the argument. The company published a Lean formalization of the proof alongside the announcement and said it does not intend to claim the Clay prize.
The effort began on 1 September after OpenAI staff heard what they called a rumour that another team was close to resolving a Millennium problem. Tristan Buckmaster and Levent Alpoge have been working on related ground. OpenAI said it contacted both men, offered a concurrent release, and offered them the prompts and the proof. Buckmaster said publicly that he had not seen the proof, did not know what the model did, and did not know whether his data had been used. He also said he was not accusing anyone of anything.
That exchange is the part of the story that matters for priority. Millennium problems are not contest entries. They are claims that other mathematicians must be able to read, reproduce and attack. A Lean file helps. Access to the prompts helps more. Until independent readers finish that work, the claim is a claim.
OpenAI researcher Sebastien Bubeck called the result a spectacular point on a twelve-month arc in which models have started to finish problems that had sat open for decades. Those earlier wins were narrower. Navier-Stokes is watched by a larger share of the field because a proof would constrain how fluids can behave, and a counter-example would change how engineers treat blow-up risk in simulations.
The company resolved two of the four statements the Clay statement asks for. That is not the same as closing the problem. The remaining statements still sit with human authors and with anyone else running large agent swarms. OpenAI is preparing for a share sale that public reports have placed near a $1 trillion valuation. Spending eight figures of compute on a proof it will not cash is, among other things, a demonstration of capacity.
The Navier-Stokes statement Clay published in 2000 asks whether the equations that engineers already use can be trusted not to explode in finite time, and whether a smooth initial fluid stays smooth. A partial answer on two of four clauses does not retire the prize. It does change the workload. Reviewers now have to read a machine-produced Lean script at the same time as any human preprint that Buckmaster, Alpoge or anyone else posts.
Cost is part of the record. One hundred and thirty billion tokens is not a graduate student's summer. It is a bill that only a handful of companies can pay. If the proof stands, the field will have to decide whether the next open problems should wait for that bill to be paid again. If it falls, the money will still have bought a public test of how far an agent swarm can get on a problem that has resisted proof since the 1930s.