---
title: "MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2608.02295v1"
permalink: "https://feed.astralor.com/items/itm_3112dbbac485bb23803e64ad"
published: "2026-08-03T14:24:12.000Z"
score: 78
channel: "ai"
tags: ["Lean 4","Mathlib","MechGeo","Counterexample-guided diagnosis","Euclidean Geometry","Autoformalisation"]
---

# MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

## AI commentary

> The highlight of this work is integrating counterexamples into the formalization repair loop, with Lean's kernel as the final judge, truly achieving machine-checkable proofs. For researchers in automated reasoning, formal mathematics, and LLM alignment, this framework is worth serious attention, especially its large gains on weaker models, which suggest that reliable intermediate representations matter more than simply scaling models.

## At a glance

MechGeo is a Mathlib-native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. 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 with a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Across seven LLM backbones, substantial improvements in autoformalization are shown, especially for weaker direct-translation models. On 43 historical IMO geometry problems, GeoFormalizer produces formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs Lean-verified counterexamples and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems to the authors' knowledge.

## Key points

- GeoFormalizer uses GeoIR for deterministic translation and iterative repair, significantly improving autoformalization for weaker LLMs.
- GeoProver combines proof planning, intermediate lemma derivation, and selective algebraization, with all proofs and counterexamples checked by Lean's kernel.
- On 43 historical IMO geometry problems, 29 are fully automatically proved, while 14 are repaired via counterexample-guided diagnosis and proved after expert correction.
- On LEAP's Lean-IMO-Bench, MechGeo proves 12 geometry statements for the first time, formally refutes the remaining 2, and proves both repaired statements.

## Full text

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.

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_3112dbbac485bb23803e64ad