OpenAI Navier-Stokes Proof: Lean Code Doesn't Match, Paper Says

What happened

OpenAI's claim to have cracked one of mathematics' hardest open problems is facing a new and pointed challenge. A paper titled "Navier-Stokes lost in translation," posted to arXiv on October 6 by Alexander Bastounis, Fabian Circelli, and Anders C. Hansen, argues that the Lean-verified code OpenAI published does not correspond to the English-language proof it was supposed to formalize. 3 The authors, three U.K.-based mathematicians, identify two specific places where the written argument and the machine-checked version diverge. 2 Their account is that the AI introduced errors when it converted the natural-language mathematics into code. 3

The paper does not declare the proof wrong. Instead, the authors argue that a successful machine check is not a substitute for human peer review. 2 That distinction is central to the story.

How we got here

On September 8, OpenAI announced that its AI had solved the Navier–Stokes problem, which concerns how fluids move and is one of the seven Millennium Prize Problems. 13 The company said a system of 10,000 "coordinating agents," powered by an internal model, reached the result in 88 hours. 4 According to OpenAI, the agents worked in communicating groups and could run code and read from a cached version of the internet. 4 The claim drew early skepticism, including from New York University mathematician Tristan Buckmaster. 4 It also prompted a dispute over who deserved credit for the result. 3

On October 6, OpenAI went much further. It published 722 reports on GitHub, organized into 372 categories, covering core results, supporting arguments, and alternative proofs. 5 The material spans abstract algebra, mathematical physics, quantum algorithms, and differential geometry, and some of the targeted problems are more than a century old. 5 OpenAI said its model had advanced to a point where basic math benchmarks could no longer measure it well. 1

The catalogue did not hold up intact. A day after release, OpenAI withdrew three manuscripts after a sign error broke one argument and two papers that depended on it, reducing the count to 719. 2 A report published Thursday also found that the release departed from guidelines an independent panel of mathematicians had written for AI labs. 2

Why the Lean mismatch matters

Formal verification in a proof assistant like Lean was the strongest part of OpenAI's case. A Lean check is supposed to provide certainty that a stated theorem follows from its premises. But Lean can only confirm the statement it is given. If the formal statement or its definitions drift from what the human-readable proof claims, the check can succeed while confirming something other than the intended result.

That is the problem Bastounis, Circelli, and Hansen describe. 3 Their finding does not show that the Navier–Stokes argument fails. It shows that the formal certificate cannot be accepted at face value as evidence that the English proof is correct. Someone still has to check that the translation is faithful, and that work requires expert human attention.

A wider credibility question

The mismatch matters more because of the scale of the release. Reactions from mathematicians have been mixed. KAIST professor Baik Hyung-ryeol said several of the problems are at a level comparable to Fields Medal work and that verified main results would have an enormous impact. 1 Fields Medalist Terence Tao, on the day of the release, raised a different concern: problems are being "solved" by AI prompters who do not understand the output well enough to answer questions or give talks about it. 2

Taken together, these reactions point to a mismatch between output and the capacity to verify it. Hundreds of manuscripts appeared at once. Three were withdrawn within a day. The flagship result's formal check has been shown to diverge from its prose. Each of these is a specific failure, but they share a cause: production has moved faster than the community's ability to review the work.

The reading

The most reasonable conclusion is that OpenAI's mathematical claims are unresolved, not refuted. The Lean paper weakens the argument that the Navier–Stokes result is already settled by machine verification, and its authors are careful not to claim more than they have shown. 2 Formal tools remain valuable. This episode shows that they shift the verification burden onto the faithfulness of the formalization rather than removing it.

For AI-driven research to be accepted in mathematics, labs will likely need to follow the norms of the field: fewer and more carefully checked releases, authors who can defend the work, and adherence to guidelines like those the independent panel proposed. 2 Until that review happens, the claimed breakthroughs should be treated as candidates awaiting verification.