OpenAI's Navier-Stokes proof doesn't use the method the company claimed: a breakdown of 166 pages

Experts who took the text apart say it does not follow the "Spanish program", even though OpenAI wrote that it did, explicitly and more than once.

Gonzalo Cao-Labora of EPFL read all 166 pages down to the details and found a different approach.

OpenAI announced the proof on Sep 8, 2026. It was assembled by a swarm of about 10,000 copies of the company's internal math model: 88 hours of compute and 130 billion tokens. In the text itself, the company wrote explicitly and more than once that it was following the program of Diego Córdoba and Luis Martínez-Zoroa.

The dispute is no longer about whether the machine did the computation, but about what exactly it proved and what backs that up.

**The Lean checkmark is not about the original text.** Lean checks the formal version of a proof, not the prose it was translated from. The paper arXiv:2610.08144 (Bastounis, Circelli, Hansen) from Oct 6 shows this on the spot: the formalized version does not match the verbal proof of the blowup, the moment when a solution of the equation goes to infinity in finite time.

**The wrong variant of the problem was closed.** OpenAI closed variants (C) and (D) of Charles Fefferman's 2000 formulation, where blowup is allowed under a smooth external force. Luis Silvestre of the University of Chicago says the Clay problem in this setting is closed, while the main Navier-Stokes problem remains open. The Clay Institute pays $1 million for it.

The authors of the original program see the forced variant differently: Diego Córdoba considers it meaningful, because every known fluid is under some external force, while Luis Martínez-Zoroa points out that other groups worked precisely on the scenario without a force.

Tristan Buckmaster of NYU and Levent Alpöge posted their three results a few hours before OpenAI's announcement: porous media, Boussinesq, and 3D Euler with blowup under a smooth force. They obtained the Boussinesq and Euler blowups on Aug 15, 2026, and checked them in Lean on Aug 22. They worked with Claude and Codex; Buckmaster calls the first machine-written text the worst thing he has ever read, and calls his own Euler write-up neuroslop.

You can check it by hand. The repository github.com/openai/math is open under Apache-2.0: 719 manuscripts in 372 families of results, with a Lean formalization for roughly 42% of the main results. The README itself warns that unformalized results may have problems (snapshot of Oct 6, 2026).

Camillo De Lellis of the Institute for Advanced Study does not expect the dispute to be settled: in his words, it is no longer a question of verifiable mathematical facts.

OpenAI's Navier-Stokes proof doesn't use the method the company claimed: a breakdown of 166 pages

Experts who took the text apart say it does not follow the "Spanish program", even though OpenAI wrote that it did, explicitly and more than once.

Gonzalo Cao-Labora of EPFL read all 166 pages down to the details and found a different approach.

The dispute is no longer about whether the machine did the computation, but about what exactly it proved and what backs that up.

Camillo De Lellis of the Institute for Advanced Study does not expect the dispute to be settled: in his words, it is no longer a question of verifiable mathematical facts.