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.
Introduces FaithformBench, a benchmark for assessing the faithfulness of mathematical chain-of-thought autoformalisation systems by measuring validity and invalidity preservation on perturbed steps. Applied to eight AF systems, it reveals widespread sycophancy where invalid inputs are silently corrected.