The Pulse
Mathematicians Reassess OpenAI’s Navier–Stokes Proof
Mathematicians interviewed by Scientific American say OpenAI’s Navier–Stokes proof appears to use a different method from work by two researchers. A separate preprint questions whether the proof’s Lean formalization matches its written argu
AI.info Team · Written with AI ·
OpenAI’s proof of a Navier–Stokes singularity may be less indebted to other mathematicians’ work than early accounts suggested, but that does not settle whether its written argument has been verified. In a report published October 13, Scientific American said mathematicians studying the proof increasingly view its resemblance to a separate research program as superficial. A preprint published October 6 raises a different concern: the Lean code OpenAI released does not always match the stronger claims in the accompanying prose.
Experts see a different route
OpenAI announced its result on September 8, saying an internal AI system had produced an analytical proof and a Lean formalization for finite-time blow-up in the three-dimensional Navier–Stokes equations. The announcement followed work by mathematicians Tristan Buckmaster and Levent Alpöge on a related problem involving the Euler equations. Their research, and an approach developed by Diego Córdoba and Luis Martínez-Zoroa, prompted questions about whether OpenAI’s system had built on work that was not yet public.
After speaking with several groups examining OpenAI’s paper, Scientific American reported that the proof does not appear to follow the Córdoba–Martínez-Zoroa approach, often called the Spanish program. “When you go to the details, it is a different approach,” said Gonzalo Cao-Labora, a mathematician at EPFL, the Swiss Federal Institute of Technology in Lausanne. The assessment narrows the case for a direct methodological overlap; it does not establish precisely how the model arrived at its result.
The shared feature is an external force
Both approaches concern a version of the problem in which an external force acts on the fluid. OpenAI says its construction starts with a smooth fluid at rest and uses a smooth force while the fluid’s energy stays finite. The company says that result establishes options C and D in the Clay Mathematics Institute’s problem statement, which allow an external force; options A and B ask about cases without one.
That distinction matters to mathematicians interested in whether the equations can break down without a specially designed push from outside. Scientific American reported that OpenAI’s method constructs the force differently from the Spanish program, even though both use the force-permitted formulation. OpenAI has also said its internal investigation found that Buckmaster’s Codex prompts could not have influenced the system, including through training, and that it will not claim the Clay prize for the result.
A verified Lean proof is not the same as a verified translation
The separate challenge comes from Alexander Bastounis, Fabian Circelli and Anders C. Hansen. Their October 6 preprint examines whether the Lean code faithfully represents OpenAI’s natural-language proof. The authors identify discrepancies, including an estimate where the Lean formalization requires an additional input derivative compared with the written paper, and argue that Lean’s acceptance of the code alone cannot certify the prose.
“In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.”
Alexander Bastounis, Fabian Circelli and Anders C. Hansen, authors of the arXiv preprint
The authors’ finding is a criticism of the link between the two versions, not a demonstration that the underlying mathematical result is false. It leaves a practical review task: mathematicians must check the written proof itself and determine whether its steps establish the stated result.
Two questions remain separate
The debate now has distinct tracks. The October 13 review weakens the claim that OpenAI’s final method closely follows the Spanish program, while the preprint questions whether the accompanying Lean proof substantiates the prose. Neither finding, on its own, resolves the other issue.
OpenAI’s stated result is also narrower than a proof about every fluid flow: it concerns blow-up under a smooth external force, a case included in the Clay formulation. The Clay statement separates that case from the unforced options. Whether the written proof withstands independent mathematical scrutiny remains the concrete test of OpenAI’s claim.