LeanGeo: Formalizing Competitional Geometry problems in Lean

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://anonymous.4open.science/r/LeanGeo-9CE9}.