MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

Researchers have introduced MechGeo, a framework that automates the formalization and proof of Euclidean geometry problems using the Lean 4 proof assistant. The framework consists of two main components: GeoFormalizer, which translates informal geometry problems into a structured representation called GeoIR and then into Lean 4 code, and GeoProver, which constructs proof plans and derives intermediate lemmas. GeoProver can selectively algebraize subgoals, using external tools like Singular or SymPy to generate algebraic certificates, but all proofs are ultimately verified by Lean's kernel. In experiments across seven LLM backbones, MechGeo significantly improved autoformalization, especially for models with weaker direct translation abilities. On a set of 43 historical IMO geometry problems, GeoFormalizer generated formal statements that GeoProver proved in 29 cases. The framework is designed to be Mathlib native, meaning it integrates with the existing Lean mathematical library. This work addresses the challenge of faithfully converting informal mathematical statements into machine-checkable proofs, a key step for using AI in formal mathematics.