OpenAI Ran 10,000 Agents Against Navier–Stokes – and Doesn't Know What They Contributed
Experts are challenging not only whether OpenAI's 166-page candidate proof holds — they claim the company has mischaracterized its approach. At the same time, an OpenAI researcher admits that no one knows what the roughly 10,000 agents that developed the proof actually contributed.
In early September 2026, OpenAI presented a 166-page potential solution to the Navier–Stokes problem. The company claimed the proof followed the approach of the Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa. Several expert groups now dispute this characterization, according to Scientific American reporting reproduced by THE DECODER on October 17, 2026.
"When you get into the details, it's a different approach," says mathematician Gonzalo Cao-Labora at EPFL, according to the reporting. The similarities to Córdoba and Martínez-Zoroa's work are only superficial, he says.
A Proof a Machine Can Check, but No One Can Read
A central complication in the case is the form the proof is written in. It is formulated in Lean, a formal verification language that checks every logical step mechanically. That means the proof's internal consistency can be verified — but the Lean code itself does not, on its own, make the proof readable by humans.
This places the mathematics community in an unusual position: the verifiability of the system simultaneously creates a barrier to traditional peer review, in which humans read and evaluate the argument. The real resolution therefore lies with the Clay Mathematics Institute (CMI), which has been reviewing the proof since it was made public. That review is still ongoing. Until CMI reaches a conclusion, it remains unsettled whether the proof is correct — and whether it actually builds on Córdoba and Martínez-Zoroa's approach as OpenAI claims.
The Data Dispute That Will Probably Never Be Resolved
Before publication, mathematician Tristan Buckmaster at NYU accused OpenAI of building on work he and Anthropic researcher Levent Alpöge had done with publicly available models. OpenAI denied the accusation, stating that the company never used Buckmaster's data.
A definitive resolution is likely impossible, according to Camillo De Lellis at the Institute for Advanced Study: language models are black boxes, making it very difficult to document conclusively what they build upon. Both the accusation and the denial therefore remain unresolved in the record of the case.
10,000 Agents, 88 Hours — and No One Who Knows What They Contributed
The scale OpenAI deployed behind the proof is significant, according to the reporting: roughly 10,000 model instances were run for approximately 88 hours, consuming 130 billion tokens, to develop the proposed solution.
But the most striking statement comes from the company itself. According to OpenAI researcher Noam Brown, no one really knows what this massive agent swarm contributed to the result. It is a remarkable admission: the company can neither document that the result follows the approach it claims, nor explain what its own massive computing effort actually produced.
The October Dump That Provoked
The case escalated at the beginning of October, when OpenAI published roughly 400 new mathematics results — results the mathematical community can barely keep up with. They were released as a loose collection on GitHub, drawing strong reactions from mathematicians who experienced it as a devaluation of their field.
The pattern is striking: one formally checkable but unreadable candidate proof, followed by a mass publication that undergoes no traditional quality process. It is this combination — enormous speed, formal verifiability, and a lack of human understanding — that lies behind the experts' criticism. The mathematicians are disputing not only the results, but the entire way OpenAI produces and presents them.
Where the Case Stands
It is worth being clear about what is actually confirmed. The entire story rests on secondary reporting: THE DECODER cites Scientific American, and OpenAI's own materials — the Lean proof, the GitHub collection, and the company's statements — are not independently available in the reporting this article is based on.
What would change the case is a conclusion from the Clay Mathematics Institute. Until that arrives, these questions remain open: Is the Navier–Stokes proof correct? Does it follow Córdoba and Martínez-Zoroa's approach, as OpenAI claims, or a different one, as Cao-Labora says? Did OpenAI use Buckmaster's data? And what did the 10,000 agents actually contribute? The answers lie with CMI, in the black boxes — and with the company itself.
This story is based on secondary reporting from THE DECODER (db63000f), which cites Scientific American.

