MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
2026-08-03 • Artificial Intelligence
Artificial IntelligenceLogic in Computer Science
AI summaryⓘ
The authors created MechGeo, a system that helps turn informal descriptions of geometry problems into formal, verifiable proofs using the Lean 4 proof assistant. Their method uses two parts: GeoFormalizer, which translates and fixes problem statements, and GeoProver, which plans and checks the proofs, sometimes using algebra tools like Singular or SymPy. They tested their system on famous math competition problems and showed it can formally prove or disprove them with high reliability. This work demonstrates how combining automated reasoning with formal verification can improve trust in geometry problem solving.
autoformalizationLean 4Euclidean geometryformal proofGeoIRcounterexamplesymbolic computationgeometry theorem provingalgebraic certificateslarge language models (LLMs)
Authors
Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi
Abstract
We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.