Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
Summary
A scholarly preprint argues that Lean verification of AI-generated or NL-based formal proofs cannot guarantee correctness due to semantic translation challenges. The work situates semantic fidelity within the Solvability Complexity Index, suggesting autoformalisation may be harder than foundational problems like the Halting problem. It provides concrete mistranslation examples, including OpenAI's Navier-Stokes proof, showing misalignments between natural-language proofs and their Lean verifications.