Mathematicians Say OpenAI Never Understood Its Own Navier-Stokes Proof — and the 'Spanish Program' Story Was Wrong

When OpenAI announced in early September that an internal model had produced a 166-page solution to the Navier-Stokes problem — one of the Clay Mathematics Institute's million-dollar Millennium Problems — the company was clear about its lineage: the proof, officials said repeatedly, followed the approach devised by Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa. More than a month later, the mathematicians who have been picking the paper apart say that account is simply wrong.

A new Scientific American investigation quotes several expert groups who have worked through the proof, and all converge on the same conclusion. "When you go to the details, it is a different approach," Gonzalo Cao-Labora, a mathematician at EPFL in Lausanne, told the magazine. The resemblance to the Spanish program that triggered a very public dispute — NYU's Tristan Buckmaster and Anthropic researcher Levent Alpöge had spent the year advancing that program with AI tools, and cried foul when OpenAI announced its result — now looks skin-deep.

The nuance matters. Both OpenAI's proof and the Spanish program exploit the same loophole in the Clay Institute's official problem statement: the formal version permits constructing a strange, unphysical external force that "stirs" the fluid into a finite-time blowup — an infinite flow speed that cannot occur in reality, satisfying the statement's official alternatives C and D. The long-sought no-force version of the problem remains open. What the examinations now show is that OpenAI constructs its unnatural force in a completely different way; the two camps borrowed the same legal clause, not the same argument.

There is an odd wrinkle. OpenAI first used a smaller team of agents to prove an intermediate result, and some experts believe that earlier squad did follow the Spanish program. But when the company scaled up to a swarm of roughly 10,000 model instances — about 88 hours of compute and 130 billion tokens in total — the system apparently discovered that a different path was required to finish. Whether that counts as building on the Spanish work or departing from it is exactly what nobody can determine.

Because here is the deeper revelation, and it is not about attribution: OpenAI did not understand its own result. Company officials repeated the Spanish-program claim on announcement day, September 8, and only weeks later did external mathematicians establish otherwise. Even top experts have found the blowup construction impenetrable as written — the agents coded every step into the Lean proof language precisely so a machine could check what no human could comfortably read. OpenAI researcher Noam Brown has since admitted that nobody knows what the 10,000-agent swarm actually contributed; he puts less than 10 percent of the success down to the multi-agent setup itself.

Verification, in other words, is not comprehension. The Lean code certifies every logical step; it says nothing about what the system was doing or why. "I honestly don't see a factual resolution of this," Camillo De Lellis of the Institute for Advanced Study told Scientific American. "It's not anymore a matter of clearly verifiable mathematical facts." The reasoning chain of a black-box model trained on unknown data is, quite possibly, permanently unknowable — OpenAI denies its model saw Buckmaster's work, and no one can prove it either way.

The episode has already soured relations between OpenAI and the mathematics community. In October the company followed up by releasing roughly 400 more results in a loose GitHub dump — the release that prompted Terence Tao to amplify calls for a boycott. The complaint then, as now, is not that the results are fake but that the burden of understanding machine-made mathematics is being offloaded onto the humans least equipped to absorb it.

That may be the real finding of the Navier-Stokes saga. The bottleneck in AI-assisted mathematics is no longer proving — the machine can do that, and Lean can check it. The bottleneck is understanding: explaining what was done, whether it is new, and what it means. A frontier lab shipped a landmark result it could not itself interpret, and the correction came not from OpenAI but from the outside mathematicians it had, however unintentionally, eclipsed. In the race to let models do mathematics, comprehension has become the scarce resource.