TLDR: LeanGeo is a new framework built within the Lean 4 theorem prover that formalizes and solves complex geometry problems, including those from the International Mathematical Olympiad. It features a comprehensive library of theorems and a benchmark (LeanGeo-Bench) to evaluate AI models, highlighting current limitations in automated geometric reasoning. The framework also explores reinforcement learning to improve AI’s geometric problem-solving capabilities.
A new research paper introduces LeanGeo, a groundbreaking framework designed to formalize and solve complex geometry problems, particularly those found in high-level competitions like the International Mathematical Olympiad (IMO). Developed within the Lean 4 theorem prover, LeanGeo aims to bridge significant gaps in current artificial intelligence (AI) systems for mathematical reasoning.
Geometry problems are a critical test for AI’s reasoning abilities. However, existing AI systems for geometry often operate in isolation, making it difficult to combine geometry with other mathematical fields like algebra or number theory. Furthermore, verifying geometric proofs, which often rely on intuitive diagrams, is notoriously challenging. LeanGeo addresses these issues by providing a unified, rigorous framework.
A Unified Formal System for Geometry
LeanGeo builds upon the Lean 4 theorem prover, a prominent proof assistant known for its strong foundation in algebra and number theory through its extensive Mathlib library. While Mathlib previously offered limited support for Euclidean geometry, LeanGeo introduces a comprehensive library of 260 high-level geometric theorems. These theorems cover a wide range of topics, from basic middle-school geometry to advanced IMO-level concepts like Menelaus’s and Miquel’s theorems.
A key feature of LeanGeo is its ability to integrate seamlessly with Mathlib. This integration allows the system to leverage powerful tools from other mathematical areas, such as trigonometric identities and advanced inequalities, which are often beyond the scope of purely axiomatic geometry systems. This hybrid approach enables LeanGeo to tackle interdisciplinary problems common in modern competitions.
The proofs within LeanGeo are designed to be human-like and declarative, mirroring the step-by-step style of traditional geometry. This makes the proofs not only verifiable by the Lean 4 system and its integrated SMT (Satisfiability Modulo Theories) solver, CVC5, but also more intuitive and understandable for humans. The system rigorously accounts for all possible geometric cases, ensuring a higher level of soundness compared to systems that might only consider a single diagrammatic representation.
LeanGeo-Bench: A New Benchmark for AI in Geometry
To evaluate the geometric reasoning capabilities of Large Language Models (LLMs), the researchers also introduce LeanGeo-Bench. This is the first formalized geometry problem benchmark in Lean 4, comprising 122 problems from various sources, including all IMO geometry problems since 2000. The benchmark’s difficulty spans from foundational exercises to highly challenging competition-level tasks.
Baseline evaluations were conducted on LeanGeo-Bench using several state-of-the-art LLMs, including Gemini 2.5 Pro, o4-mini, Grok 4, Kimi K2, Claude 4, and Qwen3-235B-A22B. While some models showed partial success on simpler problems, their overall performance remained below 30%. Notably, none of the evaluated models could solve any of the 62 Olympic-level problems, underscoring the significant limitations of current LLMs in handling complex geometric proofs that demand sophisticated logical reasoning and formal verification.
Also Read:
- EvolMathEval: A Dynamic Approach to Challenging AI’s Mathematical Reasoning
- DeepLog: A Unified Framework for Neurosymbolic AI
Advancing AI with Reinforcement Learning
The paper also explores the use of reinforcement learning (RL) to improve LLM performance on LeanGeo. Facing the challenge of limited pre-existing data for this novel framework, the researchers developed a synthetic data generation pipeline. This process involved prompting LLMs to synthesize new theorems and proofs based on existing LeanGeo library theorems, which were then automatically verified.
An “instilling method” was also proposed to manage the large theorem library within the LLM’s context window during RL training. By randomly selecting a subset of theorems for the prompt, the model was encouraged to discern and apply truly pertinent theorems within a noisy context. This training regimen led to enhanced performance, demonstrating the potential for further advancements in automated geometric theorem proving.
LeanGeo represents a significant step towards a more robust and integrated approach to automated geometric reasoning. By providing a declarative, human-readable framework, a challenging benchmark, and initial reinforcement learning experiments, it establishes a scalable testbed for advancing neuro-symbolic reasoning in mathematics. The research paper can be found here: LEAN GEO: Formalizing Competitional Geometry Problems in Lean.
