New Paper Argues Lean Verification Fails to Guarantee Correctness of AI Autoformalised Navier-Stokes Proof

A new arXiv paper by Alexander Bastounis, Fabian Circelli, and Anders C. Hansen challenges the reliability of using formal verification tools like Lean to validate AI-generated mathematical proofs. The authors argue that the process of autoformalisation—translating natural language (NL) into formal code—fails to guarantee that the formal proof corresponds to the original NL argument due to inherent semantic ambiguities.

Computational Limits of Autoformalisation

The core argument rests on the Solvability Complexity Index (SCI) hierarchy. The paper demonstrates that resolving ambiguities in mathematical NL text to achieve a semantically faithful translation is arbitrarily high in the SCI hierarchy, specifically SCI = ∞. This implies that providing a faithful AI autoformalisation is computationally harder than any standard computational problem, including the Halting problem (which has SCI = 1).

Case Study: OpenAI's Navier-Stokes Proof

The authors apply this theory to OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations. They provide concrete examples of AI mistranslations where the formal Lean proof does not match the natural language proof. Consequently, the mechanical verification of the Lean code offers no confidence in the correctness of the original NL argument regarding the Navier-Stokes equations.