AI Autoformalization Fails to Guarantee Correct Math Proofs

Autoformalization, which uses AI to translate natural language mathematical texts into formal languages like Lean for verification, does not ensure the accuracy of the original proofs. The process faces significant challenges in semantically faithful translation due to ambiguities in mathematical natural language text, which are highly complex problems. The article demonstrates this with practical examples, including OpenAI’s announced proof of blow-up solutions to the Navier-Stokes equations, showing that the formalized Lean proof does not match the natural language proof.