Navier–Stokes Lost in Translation

The work examines the gap between mechanically verified formal proofs and the informal natural-language arguments they are meant to represent, arguing that translating mathematical text into a formal language like Lean in a semantically faithful way is fundamentally harder than any computable decision problem. It proves that resolving the ambiguities inherent in mathematical natural language sits arbitrarily high in the Solvability Complexity Index/arithmetical hierarchy (SCI = ∞), meaning semantically faithful autoformalisation is strictly harder than problems such as the Halting problem. Theoretical analysis is combined with concrete diagnostics to show that faithful meaning-preserving translation cannot be guaranteed by algorithmic procedures of any fixed computational complexity.

To illustrate the practical consequences, several real-world AI mistranslations of statements and proofs into Lean are exhibited, producing verified formal objects that do not match the intended natural-language arguments. A prominent example shows that a published Lean formalisation tied to a claimed proof of blow-up for Navier-Stokes equations does not correspond to the original natural-language proof as presented. The combination of the impossibility-style result and empirical examples leads to the clear conclusion that Lean verification of an AI-produced formalisation does not by itself guarantee the correctness of the underlying natural-language proof.