A new paper on arXiv argues that a popular method for verifying AI-generated mathematical proofs may provide false confidence in their correctness. The technique, called autoformalisation, translates mathematical arguments from natural language into formal computer languages like Lean, which can then be mechanically verified.
According to the paper, OpenAI recently announced a proof of blow-up of solutions to the Navier-Stokes equations using this autoformalisation process. However, the authors argue that even when a formal proof verifies correctly in Lean, it may not actually correspond to what the natural language proof claims.
The core problem, they explain, stems from ambiguity in natural language mathematics. Translating a mathematical argument faithfully from English (or another natural language) into formal logic requires resolving these ambiguities. The paper argues that this task of performing semantically faithful translation has a Solvability Complexity Index (SCI) rating of infinity—meaning it is theoretically harder than any computable problem, including the famous Halting problem.
To demonstrate their point, the researchers provide examples of AI mistranslations of mathematical statements and proofs into Lean. Notably, they show that the formalised Lean proof of the Navier-Stokes blow-up does not correspond to the natural language proof that was originally presented.
This finding raises questions about the reliability of autoformalisation as a verification method for AI-generated mathematics. While formal verification can confirm that a proof is logically consistent within a formal system, the paper contends that such verification does not ensure the formalised proof accurately reflects the original argument in its natural language form.
The implications are significant for AI applications in mathematics, where researchers and institutions may rely on formal verification as assurance of correctness. The work suggests that additional scrutiny of both the translation process and the original natural language proofs may be necessary before accepting such results.
Key facts
- Autoformalisation translates mathematical proofs from natural language to formal languages like Lean for mechanical verification
- The paper argues this process cannot guarantee the formal proof matches the original natural language argument
- Resolving ambiguity in mathematical natural language text has a Solvability Complexity Index of infinity, making it theoretically harder than the Halting problem
- Examples provided show AI mistranslations in OpenAI’s announced Navier-Stokes proof and other cases