MechGeo: Automatically Formalizing and Proving IMO Geometry in Lean 4
MechGeo brings autoformalization and automated proving into a single Lean 4 verification loop, taking informal Euclidean geometry problems from faithful formal statements to kernel-checked proofs or counterexamples. This post introduces the framework and reports its results on IMO geometry problems from 2000–2026 and on LEAP’s Lean-IMO-Bench.
| 44 | 12/14 | 14/14 | Lean 4 |
|---|---|---|---|
| IMO geometry problems 2000–2026 |
Original LEAP statements automatically proved |
Faithful LEAP coverage after repair |
All proofs and counterexamples checked |
I. A Unified Formalization and Proving Pipeline
We are pleased to announce MechGeo and the accompanying MechGeoBench, which is available at https://github.com/MechMath/MechGeoBench. MechGeo is a Mathlib-native framework that automatically translates an informal Euclidean geometry problem into a Lean 4 theorem and then automatically constructs a complete, kernel-checked proof. By placing autoformalization and automated proving in the same verification loop, MechGeo moves beyond evaluations that begin with manually prepared formal statements.
At the statement level, GeoFormalizer reads the natural-language problem, represents its geometric content in the typed intermediate language GeoIR, and deterministically translates it into a Mathlib-native Lean statement. Compiler diagnostics and semantic evaluation guide iterative repair, helping the system generate statements that are not only well typed, but also consistent with the informal statement.
At the proof level, GeoProver receives only the formal Lean statement. It reconstructs the configuration, develops a proof plan, derives intermediate lemmas, and selectively converts suitable geometric subgoals into polynomial constraints. Singular or SymPy may help discover algebraic certificates, but every certificate, counterexample, and final proof is checked by Lean’s kernel.
II. Benchmark-Scale Results on IMO Geometry
Using this pipeline, we constructed faithful formal statements and complete Lean proofs for 44 IMO geometry problems spanning 2000–2026. Among the 43 historical problems, GeoProver directly proved 29 automatically generated statements. For the remaining 14, it automatically produced Lean-verified counterexamples, typically exposing missing nondegeneracy or point-order assumptions. After expert repair, GeoProver proved all 14 corrected statements. MechGeo also autoformalized and proved IMO 2026 Problem 2 directly from the original informal problem. To the best of our knowledge, this is the first benchmark-scale result combining automatic statement formalization with automated, kernel-checked proof construction for IMO geometry across this period.
III. LEAP and Counterexample-Guided Repair
MechGeo also establishes a new result on the 14 geometry problems in LEAP’s Lean-IMO-Bench. GeoProver automatically proves 12 original formal statements for the first time, formally refutes the remaining two, and proves both after the missing assumptions are repaired. The directly comparable result is 12/14 on the original benchmark, with faithful verified coverage of 14/14 after validation and repair.
The key lesson is that a formal statement can compile, and may even be provable, while still misrepresenting the intended problem because of a degenerate configuration or an omitted order condition. MechGeo therefore supports a stronger workflow: autoformalize, automatically prove or refute, repair when necessary, and prove again. This counterexample-guided loop makes automated geometry both more capable and more trustworthy.