Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
Summary
This arXiv paper argues that Lean verification of AI-generated formalizations cannot guarantee correctness of the original natural-language proofs due to semantic translation challenges. It demonstrates mistranslations between NL proofs and Lean verifications, including issues surrounding OpenAI's Navier-Stokes proof, and situates the difficulty within the SCI hierarchy.