10,000 Agents, 88 Hours, One $1M Proof
OpenAI says a swarm of 10,000 AI agents proved a Navier-Stokes singularity in 88 hours. How the swarm worked, why Lean verification matters, and what builders should steal.
On this page
OpenAI says a swarm of roughly 10,000 coordinating AI agents proved a finite-time singularity in the Navier-Stokes equations in 88 hours. The argument is published with a machine-checked formalization in Lean. The Clay Mathematics Institute has not ruled on it, OpenAI says it won't claim the $1 million prize, and a rival team says OpenAI chased their unpublished approach. Everything below is as reported on September 8–9, 2026.
Takeaways
The breakthrough is a systems story, not a model story: parallel agent groups, not one long reasoning run. Lean formalization is the trust layer: machine-checked math anyone can verify, with one human step remaining. The compute bill reportedly ran into the millions of dollars, roughly 1,000x OpenAI's earlier math runs. Credit and provenance are unresolved and can't be settled by formalization: only the math can be checked.
What was actually claimed?
The Navier-Stokes equations describe how fluids flow, and whether smooth solutions can "blow up" into singularities is one of the six remaining Millennium Prize Problems. Each carries a $1 million prize, and the problem has resisted mathematicians for roughly 90 years.
According to OpenAI's write-up, the agents established statement "C" (and "D") of the official formulation, that an initially smooth fluid at rest can develop a singularity in finite time. Two caveats matter. First, as TNW notes, the version cracked leans on terms many mathematicians leave out of the problem, so whether it meets the Millennium criteria is genuinely open. Second, Quanta reports the result arrived at by a model more capable than anything public, GPT-6 Astra, released days earlier, was relegated to checking the answer.
How did 10,000 agents coordinate?
This is the part builders should study. The proof was not produced by one model reasoning at length. It was produced by a swarm running in parallel for three and a half days. Per OpenAI's account and Quanta's reporting:
Seed with a strategy, not a prompt
The attack rested on a forcing technique developed by Diego Córdoba and Luis Martínez-Zoroa: a radical departure from mainstream approaches. Direction came from humans; scale came from agents.
Scale groups, not single runs
Agents were subdivided into communicating groups of varying sizes. Roughly 100 agents worked ~50 hours on the Euler regularity disproof first; ~10,000 concurrent agents then attacked Navier-Stokes.
Give agents tools, not just context
The agents could read a cached internet and execute code. Millions of messages were exchanged: TNW cites 2.7 million and ~130 billion output tokens across the push.
Verify with a different system
After the September 5 result, formalization in Lean took another 17 hours using GPT-6 Astra. Discovery and verification ran on separate models: a pattern worth copying.
A toy sketch of the coordination shape looks like this:
type AgentGroup = { size: number; task: string; tools: ["web-cache", "exec"] };
async function swarm(groups: AgentGroup[]) {
// Independent groups explore variants in parallel...
const candidates = await Promise.all(groups.map((g) => explore(g)));
// ...then a separate verifier model checks, never the discoverer.
return verify(candidates, { checker: "independent-model" });
}The honest footnote: estimates put the wider effort at $10–22.5 million: roughly 1,000x OpenAI's earlier math runs. Swarms work; they are not cheap.
Why the Lean proof is the real story
Summer 2026 has been a binge of AI-derived math: proofs across many areas, nearly all accompanied by Lean formalizations. The reason is structural: a Lean proof can be checked by anyone running the checker, which removes trust in the claimant from the equation.
The one step machines can't do
Formalization proves a statement with certainty. Confirming the formalized statement is logically equivalent to what mathematicians set out to prove still requires humans. That equivalence gap is where the current dispute over statements "C" and "D" lives.
For builders, the pattern generalizes beyond math: any agent system whose output matters should end in an independent, machine-checkable verification step, tests, type-checkers, proof assistants, run by a different model than the one that produced the output.
What is the dispute about?
Presented as a timeline, since the facts are still moving:
- Months of quiet work: Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic, in a personal capacity) developed an approach built on Córdoba and Martínez-Zoroa's forcing technique: a direction Buckmaster says almost nobody else was pursuing. By August 22 they had a Lean-verified proof for the Euler equations.
- Sept 1: OpenAI says it heard rumors of Millennium progress and pointed a new internal model, trained from late August, described as significantly more capable than Astra, at all six open problems.
- Sept 5: OpenAI's agents reach the Navier-Stokes result, ~88 hours after launch.
- Sept 7, 11:58pm: Buckmaster publishes his results with a statement alleging OpenAI pursued the same unusual direction after getting wind of their work, raising questions about their Codex sessions and an authorship offer. France24 has the full exchange.
- Sept 8: OpenAI publishes, denies seeing the pair's work, but concedes it "cannot rule out that de-identified data derived from their usage of our products helped improve our models", and offers to recognize concurrent-work priority.
As TNW observes, a company that considered the allegation baseless does not usually respond with a priority offer within days. And as Quanta's Kakaes notes, provenance is a claim about a training process nobody outside the company can inspect: no formalization can settle it.
What builders should steal
- Parallel groups beat long runs. For search-heavy problems, many medium-sized agent groups exploring variants outperform one agent reasoning longer.
- Separate the prover from the checker. Discovery on one system, verification on an independent one. The 17-hour Lean pass is the cheapest credibility in the whole story.
- Budget honestly. The 1,000x cost jump from earlier math runs to this one is the difference between a demo and a result. Price the swarm before promising it.
- Assume provenance questions. If your agents train on user interactions, someone will eventually ask what went into the model. Have the logging answer ready: OpenAI visibly did not.
What's unresolved
Will the Clay Institute accept it?
Unknown. The Institute hasn't commented. Mathematicians must first confirm the formalized statements match the official Millennium criteria: the "C and D" caveat is doing heavy lifting until then.
Who gets credit?
OpenAI cedes priority on 3D Euler to Buckmaster and Alpöge while claiming Navier-Stokes. A joint announcement has been floated. Terence Tao's warning hangs over all of it: "It's like having machines that can lift weights for you at the gym."
As of September 9, 2026: the math is public and checkable, the prize is unclaimed by choice, and the hardest questions, what counts as a solution, and where the ideas came from, belong to humans, not agents. I'll update this post as the Clay Institute weighs in.