Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

• URL: http://arxiv.org/abs/2607.19374v1
• Date: Wed, 17 Jun 2026 15:27:17 GMT
• Title: Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
• Abstract summary: Euclean is a framework for automatically formalizing geometry in native Mathlib.<n>Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy.
• Score: 7.28030691695892
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent formal reasoning systems have reached IMO-level performance, yet they leave a fragmented landscape: algebra and number theory are handled in Lean, while geometry still relies on domain-specific languages with limited formal guarantees. This split increases the trusted computing base and hinders unified model development. Existing geometry-in-Lean efforts (LeanEuclid, LeanGeo) introduce custom axiom systems incompatible with standard Mathlib, and their small scale ($<$ 1,100 problems) limits large-scale training. Native Mathlib autoformalization of geometry, however, poses distinct challenges: implicit diagrammatic assumptions (e.g., topological configuration and non-degeneracy) must be made explicit rather than deferred to external solvers, and models must adapt to Mathlib's small, rapidly evolving geometry infrastructure. We present Euclean, a four-stage framework - constraint explication, configuration anchoring, formalization mapping, and iterative repair - for automatically formalizing geometry in native Mathlib. We construct OMNI-Geometry (768 competition problems) and Numina-Geometry (177,597 problems), the largest geometry formalization dataset in Lean. Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy. Training Goedel v2 on our formalizations improves proof success from 13.6% to 15.1%, validating dataset quality for unified neural theorem proving. Code and datasets: https://github.com/tlb-22/Euclean.

Related papers

• MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4 [5.103695715197289]
  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.
  arXiv  Detail & Related papers  (2026-08-03T14:24:12Z)
• 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)
• Proposing and solving olympiad geometry with guided tree search [63.824930029019995]
  We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving.<n>TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry.<n>TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time.
  arXiv  Detail & Related papers  (2024-12-14T04:20:47Z)
• 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.