MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

Overview

MechGeo is a Mathlib-native framework designed to bridge the gap between informal Euclidean geometry problems and machine-checked proofs in Lean 4. It addresses two primary challenges: the difficulty of faithfully translating informal geometric descriptions into formal logic, and the complexity of constructing proofs that are both structurally sound and computationally tractable. By integrating an agentic formalization pipeline with a hybrid prover that combines geometric reasoning and symbolic algebra, MechGeo provides a robust, end-to-end solution for verifying geometry theorems.

Autoformalization with GeoFormalizer

Translating geometry problems is notoriously difficult because informal statements often rely on implicit assumptions about diagrams, non-degeneracy, and configuration. MechGeo introduces GeoIR, an intermediate representation that simplifies the translation process. The framework uses a deterministic translator to map GeoIR to Lean 4, followed by an iterative repair loop. This loop uses compiler feedback and a semantic evaluator to refine statements until they are both syntactically correct and semantically consistent with the original problem. This approach significantly boosts the success rate of formalization across various large language model backbones.

Certified Proving with GeoProver

Once a theorem is formalized, GeoProver constructs a proof plan that decomposes the problem into manageable subgoals. It employs a selective algebraization strategy: instead of converting the entire problem into a massive polynomial system, it keeps high-level geometric reasoning within Mathlib and only algebraizes specific subgoals. These subgoals are discharged using external computer algebra systems (CAS) like Singular or SymPy. Crucially, the framework does not trust the CAS output blindly; it generates algebraic certificates that are verified by the Lean kernel, ensuring the final proof is mathematically rigorous.

Performance and Impact

MechGeo demonstrates strong performance on challenging benchmarks, including historical International Mathematical Olympiad (IMO) problems and the LEAP Lean-IMO-Bench. By successfully proving or refuting these problems and providing kernel-checked artifacts, the framework establishes a practical foundation for trustworthy formal geometry. The ability to not only prove theorems but also formally refute incorrect statements with verified counterexamples highlights the system's reliability in handling complex geometric configurations.