Summary
A mathematics preprint argues that Lean’s verification of a formal proof does not guarantee that the proof faithfully represents the original natural-language argument. The authors say this mismatch occurs in the formalisation of OpenAI’s announced Navier–Stokes blow-up proof.
A 25-page arXiv preprint argues that a Lean-verified proof can still fail to represent the natural-language argument it was meant to formalise. Its authors say they found such a mismatch in the formalised version of the proof of Navier–Stokes solution blow-up announced by OpenAI.
The distinction is between checking a formal proof and checking the translation that produced it. Lean is a proof assistant: it checks whether a proof follows from a statement written in its formal language and the definitions and rules used there. That check concerns the encoded statement. Establishing that the statement faithfully captures an informal mathematical argument is a separate task.
Where the translation can go wrong
Mathematical writing can contain ambiguities that a formal version must resolve. An AI system translating an argument into Lean has to choose a precise interpretation. If that choice changes the meaning, the resulting proof may be valid in Lean while diverging from the original natural-language claim.
The preprint’s authors report several examples of AI mistranslations of mathematical statements and proofs into Lean. They include OpenAI’s announced Navier–Stokes proof, and the authors conclude that its formalised Lean proof does not correspond to the natural-language proof of blow-up.
Their broader theoretical argument concerns the difficulty of resolving ambiguities while preserving meaning. They place that problem arbitrarily high in the Solvability Complexity Index and arithmetical hierarchies, reporting SCI = ∞. The abstract describes this informally as harder than any computational problem, including the Halting problem, which it assigns SCI = 1. This is the authors’ complexity-theoretic characterisation of faithful translation, rather than a measurement of a particular AI system’s performance.
What Lean verification establishes
The paper’s argument does not concern whether Lean can check a formal proof. It highlights that a successful check alone addresses only the proof as encoded. If the translation has changed the intended statement or reasoning, verification of that formal version cannot settle whether the original argument has been proved.
That distinction is relevant whenever natural-language mathematics is converted into machine-checkable form: confidence in the final proof depends both on the formal checker and on the semantic fidelity of the translation. The work is an arXiv preprint by Alexander Bastounis, Fabian Circelli and Anders C. Hansen, submitted on 6 October 2026.