The paper, titled 'Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs,' examines the use of AI to translate natural language mathematical arguments into formal proof languages such as Lean. It notes that once translated, the formal proof can be mechanically verified, but questions whether this verification provides confidence in the original natural language argument. The authors focus on OpenAI's announced proof of blow-up of solutions to the Navier-Stokes equations as a prominent example of AI autoformalisation, where they show that the formalised Lean proof does not correspond to the natural language proof of blow-up.
The authors argue that the core difficulty lies in resolving ambiguities inherent in natural language mathematical texts. They show that this problem is arbitrarily high in the Solvability Complexity Index (SCI) hierarchy, meaning it is more difficult than any computational problem, including the Halting problem (which has an SCI of 1). Consequently, creating a semantically faithful translation from natural language to a formal language like Lean is, in principle, harder than solving any algorithmic problem, implying that no general method can guarantee a faithful translation for all mathematical texts.
To demonstrate this, the paper provides several examples of AI mistranslations of natural language statements and proofs into Lean, resulting in mismatches between the natural language proofs and their Lean verifications. In the case of OpenAI's Navier-Stokes proof, the formalised Lean proof does not correspond to the natural language proof of blow-up. This means that even though the Lean proof may be correct in its own right, it does not accurately represent the original natural language argument that the AI was supposed to have formalized, thereby undermining the confidence that Lean verification offers in the correctness of the original NL proof.