10,000 agents, 88 hours, 130 billion tokens: OpenAI's Navier-Stokes run and its verifier gate

On September 8 OpenAI announced that an unreleased internal model, coordinating on the order of 10,000 parallel agents with a cached copy of the internet and code execution, had produced a proof of finite-time singularity for the Navier-Stokes equations and formalized it in Lean. The run took 88 hours, exchanged 2.7 million messages and generated roughly 130 billion output tokens, plus about 17 more hours to formalize the result in Astra and Lean. If the proof holds, it is the second of the seven Millennium Prize problems to have a solution.

The numbers, and what they imply about the architecture

Divide them out. 130 billion tokens over 88 hours is about 1.5 billion output tokens per hour, sustained, which is a serving problem before it is a reasoning problem. 2.7 million messages across 10,000 agents is roughly 270 messages per agent, and 130 billion tokens over 2.7 million messages is around 48,000 tokens per message: whole proof sketches and code files, not chat turns.

The part that makes the result trustworthy is not any of those. It is the Lean gate. A generator, however large, produces candidates. A proof assistant either checks the candidate or it does not, and it does not care how many agents voted for it. Credibility comes from verification, not generation.

Token economics of a fleet

130 billion output tokens is a seven-figure bill at any frontier list price on /prices, and that is before the internal model's actual cost, which OpenAI has not disclosed. But the shape scales down, and the shape is what I would copy:

• Many cheap explorers, one expensive verifier. The fleet's value is coverage of the search space. The verifier's value is that it can say no with certainty.
• Cached inputs, uncached outputs. A cached internet means the expensive tokens are the ones the agents produce, which matches where 130 billion came from.
• Messages, not turns. Long messages with whole artifacts attached are cheaper per unit of progress than short conversational turns, because each one gives the verifier something concrete to reject.

Ten thousand agents did not make the proof true; a proof checker did, and every fleet you build needs its own version of that gate before the fleet size matters.

When many agents beat one big model

Not always, and the conditions are specific:

• The verifier is cheap and exact. Lean, a test suite, a compiler, a type checker. If the only judge is another model, the fleet amplifies the judge's bias.
• The search space is wide and the answer is checkable. Proofs, bug fixes with reproducible tests, optimizations with a benchmark.
• Partial results compose. Agents can hand each other lemmas, or subtasks, or failed attempts worth not repeating. The 2.7 million messages are that composition.
• You can afford the wasted tokens. Most of 130 billion tokens went into candidates that were rejected. That waste is the method, and it has to be in the budget.

For a coding team the practical version is a parallel fleet with the test suite as the gate, and a rule that nothing reaches a human without a green run. Whether it is one model orchestrating others, as in the Fable 5 orchestration pattern, or a flat fleet, the gate matters more than the topology.

The credit dispute

By September 10 there was an argument about authorship. Tristan Buckmaster at NYU and Levent Alpöge at Anthropic had been doing parallel work on the same problem, and Buckmaster has asked whether OpenAI accelerated its effort after seeing their progress. OpenAI denies any improper access. I cannot adjudicate that. It is worth noting because it previews a question every fleet run will raise: a model with a cached internet has read everyone's preprints, and "independent" is going to need a definition.

The honest gap

Everything above is OpenAI's account of an internal, unreleased model on a run nobody outside OpenAI can reproduce. The Lean formalization is the checkable part, and until it is public and independently verified, "solved" should be read as "claimed and formalized". The token and message counts are OpenAI's figures, and my economics are arithmetic on them, not measurement. And the credit dispute is unresolved. What the run does establish, regardless of how the authorship question settles, is that fleet plus verifier is a real method at scale, and that the verifier is the part worth building first.