AI 中文总结
MechGeo是基于Mathlib的智能体框架，可在Lean 4中自动形式化欧几里得几何问题并构造认证证明，在43道IMO几何题及Lean-IMO-Bbench上取得显著成果，为可信形式几何提供实用基础。
AI 中文摘要
我们提出了MechGeo，这是一个基于Mathlib的智能体框架，可共同解决欧几里得几何的忠实自动形式化与认证证明构造问题。在该框架中，GeoFormalizer以GeoIR表示非形式化问题，确定性地将其转换为Lean 4，并通过结构诊断和语义评估迭代修复候选命题。GeoProver构建几何证明规划，推导中间引理，并通过Lean中已验证的库选择性地对合适的子目标进行代数化。Singular或SymPy可生成代数证书，但所有生成的证明和反例均由Lean的内核检查。对7种大语言模型（LLM）骨干的实验显示，自动形式化取得了显著改进，尤其是对于直接翻译性能较弱的模型。在43道历史国际数学奥林匹克（IMO）几何题上，GeoFormalizer生成的形式化命题被GeoProver证明的有29例；对于剩余14例，它构造了经Lean验证的反例，并在专家修正后证明了所有修复后的命题。结合IMO 2026第2题，据我们所知，这产生了已报道的最大规模的、自动化的、经内核检查的Lean IMO几何题证明集合。在LEAP的Lean-IMO-Bench中的14道几何命题上，MechGeo首次证明了其中12道，正式反驳了剩余2道，并证明了2道修复后的命题。这些结果确立了反例引导诊断、几何推理和认证符号计算作为可信形式几何的实用基础。
英文摘要
We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.
Comments43 pages
