Researchers Say OpenAI's Lean Navier-Stokes Proof Doesn't Match Its Written Proof
A King's College London and Cambridge preprint finds the machine-checked version proves weaker or different statements than the paper mathematicians read.
Published
Last updated / Fact-checked on
Mathematicians at King's College London and the University of Cambridge say the Lean version of OpenAI's Navier-Stokes proof does not faithfully match the written proof. In at least one place, the computer-checked code proves a weaker statement. They do not claim OpenAI's result is wrong, but say the Lean check cannot vouch for the paper humans read.
Image: Illustrative photo of a fountain pen writing on lined paper. Aaron Burden / Unsplash via Wikimedia Commons — CC0
What the researchers found
OpenAI announced on September 8 that it had found a solution to the Navier-Stokes problem, one of the best-known open problems in mathematics, New Scientist reported. It published two versions: a natural-language paper and a formalization in Lean, a language that lets a computer mechanically check each logical step.
The preprint, by Alexander Bastounis of King's College London and Fabian Circelli and Anders Hansen of Cambridge, compares the two. Its key example is Lemma 8.6. According to the paper, the written proof bounds an output using four extra derivatives of the input (m + 4), while the related Lean code uses five (m + 5). That makes the Lean result mathematically weaker.
A second example concerns a pressure-flux bound. The authors say the Lean version proves a different bound by a substantially different argument, so the two are hard to compare.
King's College London highlighted the work on October 27. Its release says the finding "does not yet establish that OpenAI's original proof is incorrect." The preprint has not been peer reviewed.
| Item | Written proof | Lean version |
|---|---|---|
| Lemma 8.6 estimate | m + 4 derivatives | m + 5 derivatives (weaker) |
| Pressure-flux bound | Stated in one quantity | Extra quantity, different method |
| Verdict on OpenAI's result | Not judged by authors | Not judged by authors |
Why mistranslation happens
Hansen told New Scientist that the AI must produce Lean code that compiles. If part of the written argument won't compile, it looks for a workaround, even if that departs from the original text.
OpenAI's GitHub repository describes the code as Lean 4 formalizations of the results in its paper, the preprint notes. The authors argue that wording implies a faithful translation the code doesn't deliver.
The paper also makes a theoretical claim. Using the Solvability Complexity Index (SCI) hierarchy, a framework for classifying how hard computational problems are, the authors argue that resolving ambiguities in mathematical prose, a step needed for a faithful translation, sits at SCI = infinity. Informally, they say, that makes faithful autoformalization harder than the Halting problem.
OpenAI's response
OpenAI told New Scientist it is aware of the mismatch and that it doesn't make either proof invalid. The company said it will fix errors in the written proof as they are found. It also said it will keep formalizing the 722 math papers it released in early October, only some of which come with Lean proofs.
Not everyone reads the gap as a threat to the result. Kevin Buzzard of Imperial College London told New Scientist he is "confident that the Navier-Stokes problem has been correctly resolved" but "far less confident that the proof described in the PDF is correct."
Why it matters
Lean is increasingly treated as a stamp of correctness for AI-generated mathematics. This work suggests the stamp covers the theorem statement and the code, not necessarily the human-readable argument beside it.
That matters because mathematicians build on written proofs, not just final results. If an AI silently changes the argument to get code to compile, reviewers could approve a paper whose reasoning was never checked.
What to do with AI math claims now:
- Treat a compiled Lean proof as verifying its own statement, not the accompanying PDF.
- Check whether the formal statement was written or reviewed by humans.
- Look for independent human review before citing intermediate lemmas.
- Watch for OpenAI's corrections to the written proof and peer review of the preprint.
More coverage is on our Artificial Intelligence hub.
How we reported this
We read the arXiv preprint in full, including its Lemma 8.6 comparison, and checked it against King's College London's October 27 release and New Scientist's October 8 report, which carried OpenAI's response. We cut claims about which OpenAI model did the formalization and how many agents were used, because we could not confirm them in these sources. The comparison table is our own summary of the preprint.
Published and fact-checked October 30, 2026.
Sources
- King's College London, "OpenAI's Navier-Stokes proof called into question," Oct. 27, 2026: https://www.kcl.ac.uk/news/openais-navier-stokes-proof-called-into-question
- Bastounis, Circelli and Hansen, "Navier-Stokes lost in translation," arXiv preprint: https://arxiv.org/abs/2610.08144
- New Scientist, "OpenAI mistranslated mathematics into code for its Navier-Stokes proof," Oct. 8, 2026: https://www.newscientist.com/article/2592824-openai-mistranslated-mathematics-into-code-for-its-navier-stokes-proof/
DailyMech used AI tools to help research and draft this article; it was fact-checked by our editors.