# LeanGeo: Formalizing Competitional Geometry problems in Lean

arXiv: https://arxiv.org/abs/2508.14644 · HTML: https://mlsanity.com/paper/2508.14644/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Placed in Spatial and embodied reasoning, one of 17 directions in LLM reasoning.
- Builds on 16 of its 48 references that are in the map.
- First posted on arXiv 20 Aug 2025.

## Placed in

- LLM reasoning / [Spatial and embodied reasoning](https://mlsanity.com/lr/spatial-and-embodied-reasoning/)

## Builds on (most cited first, 16 of 16)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Kimi k1.5: Scaling Reinforcement Learning with LLMs](https://mlsanity.com/paper/2501.12599/) (2025)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning](https://mlsanity.com/paper/2105.14517/) (2021)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [GeoEval: Benchmark for Evaluating LLMs and Multi-Modal Models on Geometry Problem-Solving](https://mlsanity.com/paper/2402.10104/) (2024)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics](https://mlsanity.com/paper/2505.03171/) (2025)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?](https://mlsanity.com/paper/2506.06034/) (2025)
- [Lean-SMT: An SMT tactic for discharging proof goals in Lean](https://mlsanity.com/paper/2505.15796/) (2025)

## Built on by (most cited first, 7 of 7)

- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [LAMP: Lean-based Agentic framework with MCP and Proof Repair](https://mlsanity.com/paper/2606.28841/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [MIRROR: Learning from the Other View for Multi-Modal Reasoning](https://mlsanity.com/paper/2607.21552/) (2026)
- [An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development](https://mlsanity.com/paper/2509.02758/) (2025)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry](https://mlsanity.com/paper/2608.14585/) (2026)

## Abstract (arXiv)

Geometry problems are a crucial testbed for AI reasoning capabilities. Most existing geometry solving systems cannot express problems within a unified framework, thus are difficult to integrate with other mathematical fields. Besides, since most geometric proofs rely on intuitive diagrams, verifying geometry problems is particularly challenging. To address these gaps, we introduce LeanGeo, a unified formal system for formalizing and solving competition-level geometry problems within the Lean 4 theorem prover. LeanGeo features a comprehensive library of high-level geometric theorems with Lean's foundational logic, enabling rigorous proof verification and seamless integration with Mathlib. We also present LeanGeo-Bench, a formal geometry benchmark in LeanGeo, comprising problems from the International Mathematical Olympiad (IMO) and other advanced sources. Our evaluation demonstrates the capabilities and limitations of state-of-the-art Large Language Models on this benchmark, highlighting the need for further advancements in automated geometric reasoning. We open source the theorem library and the benchmark of LeanGeo at https://github.com/project-numina/LeanGeo/tree/master.