Navier–Stokes Lost in Translation
Points and comments are a snapshot, not live.
Faithful autoformalisation of natural language math is harder than any computational problem.
The paper argues that verifying AI-generated mathematics via autoformalisation into Lean does not guarantee the correctness of the original natural language (NL) proof. It proves that resolving ambiguities in mathematical NL text is arbitrarily high in the Solvability Complexity Index hierarchy (SCI=∞), making semantically faithful translation harder than the Halting problem. Examples of AI mistranslations are given, including OpenAI's Navier-Stokes proof, where the formalised Lean proof does not correspond to the NL proof of blow-up. The study highlights fundamental limits of using formal verification to validate AI-produced mathematical arguments.
What commenters are saying
Commenters largely agree that the paper highlights a real issue: natural language math is inherently ambiguous, and formal verification of an AI's translation does not guarantee the original proof is correct. One commenter shares a personal experience formalizing a CS paper in Lean, finding several mistakes in the original that were corrected but resulted in a different system than printed. A key point raised is that if the Lean proof proves blowup for Navier-Stokes but uses a different method than the NL proof, the NL proof may be unsound even if the statement is true. Two camps emerge: those who see this as a caution about AI-generated proofs and those who view the formal verification itself as valuable despite translation drift.