Getting the (In)Formal Statement Right (www.robertj1.com)

Recent advancements in autoformalization have highlighted the transformative impact of large language models (LLMs) on mathematics and formal proofs. OpenAI's model successfully demonstrated the finite-time blowup for the Navier-Stokes equations, with another model quickly formalizing the proof in Lean. Anthropic's model generated an extensive 13 million lines of Lean code for Fermat's Last Theorem in just 11 days. These achievements indicate a significant leap toward comprehensive formalization and verification of mathematical proofs, termed "proof abundance," allowing researchers to generate and validate proofs at unprecedented scales. However, a crucial challenge remains: ensuring the semantic fidelity of formalized statements. The issue arises when a proof, though correct within Lean, could correspond to a weaker or different mathematical claim than intended. As detected in specific examples, discrepancies between the formalized statement and the original intent illustrate the necessity for careful evaluation of both proofs and the mathematical meanings they convey. To address this, a set of checks is proposed, including freezing the statement for comparison, verifying the use of axioms, and employing both agents and human scrutiny. This multi-faceted approach aims to build trust in the proofs generated by AI systems, ensuring that they are not only correct but also accurately reflect the original mathematical statements.