MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

Summary (Overview)

• MechGeo is a Mathlib-native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry in Lean 4.
• The framework consists of two main components: GeoFormalizer (translates informal geometry problems into Lean 4 statements via an intermediate representation called GeoIR) and GeoProver (constructs geometric proof plans, selectively algebraizes subgoals, and produces kernel-checked proofs).
• On 43 historical IMO geometry problems, MechGeo proves 29 original formalizations and constructs Lean-verified counterexamples for the remaining 14, all of which are subsequently proved after expert repair—yielding the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems.
• On LEAP's Lean-IMO-Bench, MechGeo proves 12 of 14 geometry statements for the first time, formally refutes the remaining two (revealing missing nondegeneracy assumptions), and proves both repaired statements.
• The system demonstrates that counterexample-guided diagnosis, geometric reasoning, and certified symbolic computation form a practical foundation for trustworthy formal geometry.

Introduction and Theoretical Foundation

Background and Motivation

Large language models (LLMs) now solve difficult competition problems, while formal reasoning systems increasingly construct machine-checked proofs. Lean 4 provides a rigorous foundation by representing mathematical claims precisely and checking proof terms with a small trusted kernel, supported by Mathlib, a large library of formalized mathematics.

Recent systems span specialized provers and agentic frameworks: AlphaProof, Seed-Prover, and Aristotle have demonstrated Olympiad-level formal reasoning, while DeepSeek-Prover-V2, Goedel-Prover-V2, and Hilbert have advanced Lean theorem proving. However, most evaluations begin with already formalized statements, leaving open a prior challenge: faithfully translating the intended configuration into a formal statement.

Challenges in Euclidean Geometry Formalization

Faithful formalization is challenging because informal geometry problems derive meaning jointly from text, diagrams, and geometric conventions, often leaving necessary order and nondegeneracy conditions implicit. For example, "D lies on BC" may mean:

• D lies on the supporting line
• D lies on the closed segment
• D lies strictly between B and C (with $B \neq C$ often left implicit)

These interpretations yield different Lean statements, all of which may elaborate, and some may even admit valid proofs. Neither compiler feedback nor human inspection alone reliably determines whether a formal statement captures the intended configuration.

Proving formalized theorems requires exposing enough geometric structure for effective proof search. Specialized systems like AlphaGeometry achieve strong performance through specialized languages and symbolic deduction, but their success depends on proposing required auxiliary constructions. AlphaGeometry2 can express 88% of IMO geometry problems from 2000–2024; the remaining cases involve inequalities, nonlinear relations, or three-dimensional configurations.

Theoretical Foundation: Algebraic Reasoning

Algebraic reasoning is a central tool for geometry theorem proving. Coordinate algebraization translates geometric hypotheses and goals into polynomial equations and inequalities, handled systematically by:

• Wu's method [Wu, 1986]
• Gröbner basis computation [Buchberger, 1970]

Although algebraic methods reduce dependence on auxiliary constructions, algebraizing an entire configuration may produce large polynomial systems with substantial expression growth. Geometric reasoning and algebraic computation are therefore complementary: the former preserves geometric structure and decomposes theorems into manageable subgoals, while the latter systematically discharges polynomial consequences.

Methodology

3.1 GeoFormalizer: Autoformalization via GeoIR

GeoFormalizer comprises four stages:

3.1.1 GeoIR Generation

GeoIR provides a simple, compact, typed language in which models can state geometric content without directly manipulating Lean syntax. This reduces the burden of knowing Lean's type system and Mathlib interfaces.

3.1.2 Formal Statement Translation

There are four categories of GeoIR constructs: declarations, constructions, geometric relations, and values. Each has a fixed, deterministic translation in Lean performed by a rule-based translator (no LLM involved). The translator parses a geometry proposition into a typed abstract syntax tree and reconstructs the corresponding Lean statement using a fixed mapping table.

3.1.3 Evaluation

Semantic and structural signals are combined into a single score:

$$F = 0.7 \, S_{\mathrm{judge}} + 0.3 \, S_{\mathrm{struct}}$$

• The judge score $S_{\mathrm{judge}}$ evaluates correspondence between the informal problem and the generated Lean statement, assigning labels: semantically consistent (1), partially consistent (0.5), or inconsistent (0).
• The structural score $S_{\mathrm{struct}}$ is the point coverage ratio: the fraction of points declared in GeoIR that appear in the informal problem.
• The threshold $\tau = 0.6$ is chosen so $S_{\mathrm{struct}}$ is decisive only in the ambiguous case $S_{\mathrm{judge}} = 0.5$.

3.1.4 Iterative Repair

Generated GeoIR is statically checked for undeclared objects, arity errors, type mismatches, and malformed structures. Candidates receive score $F$ and are accepted if $F \geq 0.6$; otherwise, feedback is returned for revision.

3.2 GeoProver: Integrating Geometric and Algebraic Reasoning

GeoProver combines geometric and algebraic reasoning in a four-stage agentic workflow:

3.2.1 Proof Planning

The proof agent receives only the formal Lean statement, reconstructs the geometry, and organizes key lemmas, auxiliary constructions, angle chases, and algebraic identities into an ordered informal proof plan. This decomposition precedes algebraization, so each CAS call typically handles a smaller, lower-degree polynomial subsystem.

3.2.2 Selective Algebraization

Algebraization is implemented by verified lemmas and the simplification tactics to_poly and to_basic. The process proceeds in two logical steps:

1. Derived geometric predicates and objects are expressed with basic notations (vectors, norms, inner products) via to_basic
2. These expressions are expanded coordinatewise into polynomials via basic_to_poly

Rewrite rules applied by to_poly are lemmas of equivalence between geometric expressions and their algebraic forms, so they never silently strengthen or weaken the statement.

3.2.3 Certified Algebraic Discharge

For polynomial equality goals with hypotheses $p_1 = 0, \ldots, p_n = 0$ and target $q = 0$, when Lean's internal tactics are insufficient, GeoProver calls Singular or SymPy to compute cofactors $c_1, \ldots, c_n$ satisfying:

$$q = \sum_{i=1}^{n} c_i p_i$$

The agent translates this identity into a Lean proof, checked by the kernel. Inequalities and nonzero constraints are handled using Lean tactics, explicit sign lemmas, and case analysis.

Independent Verification

For each input statement, GeoProver attempts either to prove it or refute it with a counterexample. An independent verifier checks that:

• A proof must match the input statement exactly
• A counterexample must formally establish its negation
• The complete file compiles without sorry and uses only permitted Lean axioms

Empirical Validation / Results

4.1 Experimental Settings

Dataset (MG200): 200 informal geometry problems across four subsets:

• 43 historical IMO geometry problems
• 77 non-IMO problems from LeanGeo-Bench
• 22 classical geometry theorems (CertiGeo)
• 58 plane geometry problems from OMNI-Geometry

Models: Seven LLM backbones: GPT-5.6-Sol, Claude Opus 4.8, DeepSeek-V4-Pro, DeepSeek-V4-Flash, Qwen3.7-Max, MiniMax-M3, GLM-5.2. All experiments use Lean 4.27.0, Singular 4.4.1, and SymPy 1.13.2.

4.2 RQ1: Automatic Formalization

Across all 1,400 model–problem pairs, GeoFormalizer produces 1,354 statements that elaborate successfully (96.7%), compared with 1,159 (82.8%) for Euclean and 513 (36.6%) for direct translation.

Table 1: RQ1 results on the four autoformalization datasets. Each entry reports the number (percentage) of successfully elaborated Lean statements.

Ablation of repair rounds (setting $(r,f)$ where $r$ and $f$ denote compiler-guided and semantic-guided repair rounds):

Table 2: RQ1 ablation of repair rounds. Compiler-guided repair contributes most of the gain in elaboration rate.

4.3 RQ2: Automated Theorem Proving and Refutation

Main comparison and ablation results (all using DeepSeek-V4-Pro unless noted):

Table 3: RQ2 main comparison and cumulative ablation results.

Cross-tabulation of human semantic judgments and GeoProver outcomes (with GPT-5.6-Sol):

Table 4: Cross-tabulation showing that formal counterexample search refutes 22 statements judged faithful by humans, revealing degeneracy and order errors missed by human inspection.

Key ablation findings:

• Removing CAS reduces solved problems from 73 to 29
• Removing both CAS and the algebraization toolkit further reduces to 19
• For IMO 2008 P1, decomposition replaces a global system of 16 quadratic equations in 22 variables with six local systems of 3 quadratic equations each in 10 variables

4.4 RQ3: IMO-Level Geometry Results

Table 5: Proof and repair outcomes across three geometry evaluation sets.

Example: IMO 2007 P2 (missing nondegeneracy) — The formalization omitted the noncollinearity implicit in "ABCD is a parallelogram." A counterexample with $D = (0,0)$, $A = (1/5, 0)$, $F = G = (1/2, 0)$, $B = C = (1, 0)$, $E = (3/4, 1)$ shows $\angle DAF = \pi$ and $\angle FAB = 0$. After adding that A, B, and C are noncollinear, GeoProver proves the repaired statement.

Example: Lean-IMO-Bench Basic 028 (missing order relation) — The original formalization admitted configurations where points X and Y lie outside segments AB and AC. After requiring X and Y to lie in the interiors, GeoProver proves the repaired statement.

Theoretical and Practical Implications

Theoretical Contributions

1. Unified verification loop: Trustworthy geometry theorem formalization requires statement validation and proof construction within a unified loop—formalization cannot be separated from proof checking.

2. Counterexample-guided diagnosis: Formal counterexample search reveals semantic mismatches (degeneracy and order errors) that human inspection misses, establishing this as a practical diagnostic tool for formalization quality.

3. Selective algebraization: The hybrid approach of geometric reasoning (preserving structure, decomposing proofs) combined with selective polynomial algebraization (discharging algebraic subgoals) outperforms either approach alone.

Practical Implications

1. Mathlib-native proofs: Unlike specialized geometry systems (AlphaGeometry, TongGeometry), MechGeo produces reusable proofs embedded in the general Mathlib library, checked by the Lean kernel.

2. Model-agnostic benefits: The structured formalization pipeline substantially improves elaboration rates even for weaker LLM backbones (e.g., MiniMax-M3: from 57.5% to 94.5% elaboration).

3. Certified symbolic computation: External CAS tools (Singular, SymPy) may generate certificates, but all results are verified by Lean's kernel, ensuring trustworthiness.

4. Public benchmark: Results are publicly available in the MechGeoBench repository, enabling reproducible research.

Conclusion

MechGeo demonstrates that trustworthy geometry theorem formalization requires statement validation and proof construction within a unified verification loop. The system:

• Proves challenging geometry theorems (43 historical IMO problems + IMO 2026 P2)
• Detects incorrect formalizations through Lean-verified counterexamples (14 IMO statements refuted, then repaired and proved)
• Demonstrates the value of selective algebraization and symbolic computation (CAS contributes 44 additional proofs in ablation)

Future work will:

• Automate semantic and nondegeneracy checks
• Scale proof planning and certificate generation to broader and more challenging classes of geometry theorems

The key insight is that geometric reasoning and algebraic computation are complementary: the former preserves geometric structure and decomposes difficult proofs into manageable subgoals, while the latter systematically discharges the resulting polynomial consequences—all within a framework where every step is verified by Lean's kernel.