Navier–Stokes Lost in Translation

Researchers demonstrate that AI autoformalisation—translating mathematical proofs from natural language into formal languages like Lean for mechanical verification—does not guarantee the original natural language proof is correct. They prove that resolving ambiguities in mathematical text to ensure faithful translation is computationally harder than any solvable problem, including the Halting problem, and provide examples where AI mistranslations occurred, including OpenAI's announced Navier-Stokes proof.