MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

• URL: http://arxiv.org/abs/2608.02295v1
• Date: Mon, 03 Aug 2026 14:24:12 GMT
• Title: MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
• Abstract summary: We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry.<n>GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements.<n>GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean.
• Score: 5.103695715197289
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean [7.28030691695892]
  Euclean is a framework for automatically formalizing geometry in native Mathlib.<n>Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy.
  arXiv  Detail & Related papers  (2026-06-17T15:27:17Z)
• Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning [5.723373368342653]
  We introduce Hilbert-Geo, the first unified formal language framework for solid geometry.<n>We propose a Parse2Reason method containing two steps of first parsing then reasoning.<n>Our proposed method achieves the state-of-the-art (SOTA) performance 77.3% in SolidFGeo2k and 84.1% in MathVerse-Solid.
  arXiv  Detail & Related papers  (2026-05-11T13:42:41Z)
• Geoparsing: Diagram Parsing for Plane and Solid Geometry with a Unified Formal Language [60.70116693224378]
  We design a unified formal language that integrates plane and solid geometry, comprehensively covering geometric structures and semantic relations.<n>We construct GDP-29K, a large-scale dataset comprising 20k plane and 9k solid geometry samples collected from diverse real-world sources.
  arXiv  Detail & Related papers  (2026-04-13T15:09:56Z)
• Achieving Olympia-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learning [66.79506488139707]
  Large language model (LLM) agents exhibit strong mathematical problem-solving abilities.<n>In this work, we make the first attempt to build a medalist-level LLM agent for geometry and present InternGeometry.<n> InternGeometry overcomes the limitations in geometry by iteratively proposing propositions and auxiliary constructions, verifying them with a symbolic engine.<n>Built on InternThinker-32B, InternGeometry solves 44 of 50 IMO geometry problems, exceeding the average gold medalist score (40.9), using only 13K training examples.
  arXiv  Detail & Related papers  (2025-12-11T11:05:04Z)
• LeanGeo: Formalizing Competitional Geometry problems in Lean [22.345645897808357]
  We introduce LeanGeo, a unified formal system for formalizing and solving geometry problems within the Lean 4 theorem prover.<n>LeanGeo features a comprehensive library of high-level geometric theorems with Lean's foundational logic, enabling rigorous proof verification.<n>We also present LeanGeo-Bench, a formal geometry benchmark in LeanGeo, comprising problems from the International Mathematical Olympiad (IMO) and other advanced sources.
  arXiv  Detail & Related papers  (2025-08-20T11:55:19Z)
• TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving [106.04001249574786]
  TrustGeoGen is a data engine that generates formally verified geometric problems to establish a principled and trustworthy benchmark.<n>Our engine integrates four key innovations: 1) Multimodal Alignment, which synchronizes the generation of diagrams, text, and step-by-step solutions; 2) Formal Verification, ensuring all reasoning paths are rule-compliant; 3) Connection Thinking, bridging formal deduction with human-like logical steps; and 4) our textitGeoExplore series algorithms, which produce diverse problem variants with multiple solutions and self-reflective backtracking.
  arXiv  Detail & Related papers  (2025-04-22T10:45:23Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving [9.73597821684857]
  This is the first paper in a series of work we have accomplished over the past three years. In this paper, we have constructed a consistent formal plane geometry system. This will serve as a crucial bridge between IMO-level plane geometry challenges and readable AI automated reasoning.
  arXiv  Detail & Related papers  (2023-10-27T09:55:12Z)
• UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression [127.68780714438103]
  Two main geometry problems: calculation and proving, are usually treated as two specific tasks. We construct a large-scale Unified Geometry problem benchmark, UniGeo, which contains 4,998 calculation problems and 9,543 proving problems. We also present a unified multi-task Geometric Transformer framework, Geoformer, to tackle calculation and proving problems simultaneously.
  arXiv  Detail & Related papers  (2022-12-06T04:37:51Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  We construct a new large-scale benchmark, Geometry3K, consisting of 3,002 geometry problems with dense annotation in formal language. We propose a novel geometry solving approach with formal language and symbolic reasoning, called Interpretable Geometry Problem solver (Inter-GPS) Inter-GPS incorporates theorem knowledge as conditional rules and performs symbolic reasoning step by step.
  arXiv  Detail & Related papers  (2021-05-10T07:46:55Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.