用形式化系统解决竞赛级几何题，支持严格验证与跨领域集成。
LeanGeo: Formalizing Competitional Geometry problems in Lean
- 基于Lean 4构建统一形式化框架，实现几何命题的严谨表达。
- 在IMO等竞赛题上评估大模型表现，揭示当前自动推理的局限性。
- 开源完整定理库与基准测试，助力几何推理研究发展。
几何问题是检验AI推理能力的关键场景。现有几何求解系统缺乏统一表达框架，难以与其他数学领域融合；且多数几何证明依赖直观图形，验证难度高。为此，我们提出LeanGeo，一个基于Lean 4定理证明器的统一形式化系统，用于描述和求解竞赛级几何问题。LeanGeo包含一套高层几何定理库，依托Lean的逻辑基础，支持严格证明验证，并可无缝集成Mathlib。我们还构建了LeanGeo-Bench，一个基于国际数学奥林匹克（IMO）及其他高阶来源的正式几何基准。评估结果展示了当前顶尖大语言模型在此基准上的能力与局限，凸显了自动化几何推理进一步发展的必要性。LeanGeo的定理库与基准已开源：https://github.com/project-numina/LeanGeo/tree/master。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。