LeanGeo: Formalizing Competitional Geometry problems in Lean
Chendong Song · Zihan Wang · Frederick Pu · Haiming Wang · Xiaohan Lin · Junqi Liu · Jia LI · Zhengying Liu
We introduce LeanGeo, a novel framework for formalizing and solving competition-level geometry problems in Lean 4, along with a benchmark of 122 problems to evaluate the geometric reasoning capabilities of large language models.
摘要
Geometry problems constitute a crucial testbed for AI reasoning. Most existing geometry solving systems rely on domain-specific formal languages that cannot integrate with other mathematical fields, and their dependence on graphical intuition makes rigorous verification particularly challenging. To address these limitations, we introduce \textbf{LeanGeo}, a unified formal framework for expressing and proving competition-level geometry problems within the Lean~4 theorem prover. LeanGeo provides a comprehensive library of 260 high-level geometric theorems grounded in Lean's foundational logic, enabling rigorous proof verification and seamless integration with Mathlib. We further present \textbf{LeanGeo-Bench}, a benchmark of 122 formally verified geometry problems ranging from foundational exercises to International Mathematical Olympiad (IMO) challenges. Our evaluation of state-of-the-art Large Language Models on this benchmark reveals both capabilities and fundamental limitations in automated geometric reasoning. We open-source the theorem library and benchmark at \url{https://github.com/project-numina/LeanGeo}.