Tag
This paper argues that Lean verification of AI autoformalisation does not guarantee the correctness of the original natural-language proof, showing that semantically faithful translation is undecidable in the Solvability Complexity Index hierarchy. The authors demonstrate practical AI mistranslations, including a mismatch in OpenAI's announced Navier–Stokes blow-up proof.