A paper argued a Lean-checked proof is not a correct one
A preprint posted on 6 October contends that checking an AI-generated proof in Lean does not establish that the proof is right. The paper, by Alexander Bastounis, Fabian Circelli and Anders Hansen, examines autoformalisation — an AI system translating a natural-language proof into a formal language so a machine can check it — and argues the translation can be semantically unfaithful while the formal version still compiles cleanly. The authors place the problem of resolving ambiguity in mathematical prose arbitrarily high in the Solvability Complexity Index hierarchy, informally harder than the Halting problem.
They then give worked examples of AI mistranslations of statements and proofs into Lean, including OpenAI’s announced proof of blow-up of solutions to the Navier-Stokes equations, and say the formalised proof does not correspond to the natural-language argument. The claim is narrow and specific: not that the mathematics is mistaken, but that a Lean check verifies the machine’s translation of it, and nothing guarantees that translation was faithful.
WHY IT MATTERS
This is the verification story that sits underneath every “the model proved it in Lean” claim, and it is aimed squarely at OpenAI’s headline mathematics result. For a builder the lesson generalises well past mathematics: any pipeline where a model converts an artifact into a form you can check — a schema, a test suite, a policy, a formal spec — inherits exactly this gap, because the machine verifies its own translation rather than your intent, and the gap widens with the freedom you give the model. The authors are not scaling sceptics; Hansen’s group has published on the limits of general-purpose computation, and the argument here is a specific complexity result about ambiguity rather than a blanket dismissal. The caveat deserves one line: this is a preprint, not yet peer-reviewed.