Paper argues a passing Lean check does not prove an AI translated proof is right
A new paper shows that when AI translates a math proof into Lean, passing the Lean check says nothing about whether the original proof is right. They show a chatbot turning a wrong proof into a valid Lean proof by silently fixing the error. Knowing when a statement can be translated faithfully is provably harder than the Halting problem, so no AI translator can always do it.
Context
Formal verification in Lean is one of the main reasons people give for trusting AI math results.
The paper, "Navier Stokes lost in translation" by Alexander Bastounis of King's College London and Fabian Circelli and Anders C. Hansen of the University of Cambridge, was posted to arXiv on October 6. It argues that no algorithm can guarantee a faithful translation of ambiguous mathematical text into Lean, and it uses OpenAI's announced Navier Stokes proof as a worked example. It is circulating during the debate over OpenAI's release of 722 AI written math manuscripts.
Deep dive
The authors separate two jobs. One is turning an alleged proof into a Lean proof that compiles. The other is translating a whole text faithfully, definitions and arguments included. They warn that success at the first job says nothing about whether the original written proof is correct, because the AI can change the argument until Lean accepts it.
They give simple examples. When they handed ChatGPT 6 (Astra Ultra) a wrong proof about a cubic polynomial, it returned a valid Lean proof by quietly fixing the wrong root multiplicities. In another case, a correct proof was replaced by a different argument.
They then compare OpenAI's Navier Stokes paper with its Lean repository at a specific commit. For Lemma 8.6, the paper claims a bound needing four extra derivatives, while the Lean code uses five, which makes it a weaker result. For a pressure flux bound, both the statement and the method differ. The authors stress that they make no claim about whether OpenAI's written proof is correct, only about the translation.
On theory, they argue that resolving ambiguity in mathematical text is harder than the Halting problem, using results tied to Hilbert's tenth problem. They also cite the Lean community's rebuttal of a spring 2026 Meta claim to have formalized 26 textbooks.
What to expect next
The authors say the likelihood of substantial mistranslations in OpenAI's companion Euler proof is very high, based on preliminary checks, and invite others to examine it. They also say work on trustworthy autoformalization will appear in forthcoming articles.
Watch for a response from OpenAI on the Lean mismatches, for independent reviews of the Navier Stokes and Euler formalizations, and for whether journals and referees start asking that AI generated proofs be checked against their written versions, not only compiled in Lean.