This paper demonstrates that AI autoformalisation of natural language mathematical proofs into formal languages like Lean does not guarantee fidelity to the original argument. The authors prove that semantically faithful translation is arbitrarily hard (SCI = ∞, beyond the Halting problem) and provide concrete examples, including showing that OpenAI's claimed Lean verification of the Navier-Stokes blow-up proof does not correspond to the actual natural language proof.
Background
Autoformalisation uses AI to translate natural language mathematics into formal proof languages like Lean for mechanical verification. OpenAI recently announced a proof of blow-up of solutions to the Navier-Stokes equations using this approach, which has sparked discussion about the reliability of such methods.
- Source
- Lobsters
- Published
- Oct 9, 2026 at 01:16 AM
- Score
- 8.0 / 10