Imagine you write a contract in English, then ask someone to translate it into Mandarin for a Chinese court. The Mandarin version passes every legal check — grammar, structure, internal consistency. The court stamps it valid. But the translator quietly changed "exclusive license" to "non-exclusive license" because the English was ambiguous, and the translator resolved the ambiguity wrong. The court verified the Mandarin contract, not the English one. You have a stamp that means nothing. That is exactly what is happening with AI autoformalisation of mathematical proofs. The pipeline works like this: an AI writes a proof in natural language (NL), then a second AI (or the same one) translates it into a formal language like Lean 4, and Lean's kernel mechanically checks the formal version. When the formal version passes, the claim is that the original NL proof has been "verified." This paper demonstrates, with both theoretical machinery and practical examples, that the translation step is where the entire edifice collapses — and that this collapse is not a bug to be fixed but a fundamental computational barrier. The theoretical core is striking. The authors invoke the Solvability Complexity Index (SCI) hierarchy, a framework from computational mathematics that classifies problems by how many limits you need to compute to solve them. The Halting problem sits at SCI = 1. The problem of faithfully disambiguating mathematical natural language — resolving what a sentence actually means when multiple formal interpretations are valid — sits at SCI = ∞. Informally: faithful autoformalisation is harder than any problem with a finite SCI, including the Halting problem. This is not a "we need better models" argument. It is a "this problem is structurally impossible for any computational procedure" argument. The practical demonstrations are equally damaging. The authors examine OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations — a result with enormous significance if true, since Navier-Stokes regularity is a Millennium Prize Problem. They show that the Lean formalisation does not correspond to the NL proof. Specific mismatches include altered assumptions, changed boundary conditions, and formalised lemmas that prove statements different from what the English text claims. The Lean kernel happily verified the Lean code. It just wasn't verifying the proof OpenAI announced. The paper provides additional examples of AI mistranslation in practice: cases where ambiguous NL statements admit multiple formal readings, and the AI picks one that is easier to prove but semantically different from the intended claim. These are not edge cases or adversarial attacks. They are routine consequences of the gap between the looseness of mathematical English and the precision required by a formal kernel. Every working mathematician knows this gap exists — the contribution here is showing it is computationally unbridgeable. What makes this especially important is the institutional context. AI labs are increasingly using autoformalisation as a credibility signal: "our proof was verified in Lean" is becoming shorthand for "our proof is correct." This paper shows that shorthand is misleading. Lean verification confirms the formal artifact is internally consistent. It says nothing about whether that artifact faithfully represents the NL argument. The verification is real; the confidence it provides about the original claim is not. The implications extend beyond any single proof. If the AI verification pipeline becomes the default trust mechanism for AI-generated mathematics, and if the translation step is fundamentally unreliable, then the entire pipeline is a confidence-laundering machine — converting unverified NL claims into formally-stamped artifacts that carry unearned authority. The authors are not saying formal verification is useless. They are saying it verifies the wrong thing when the input is a lossy translation from natural language.
