MechGeo：在Lean 4中自动形式化并证明欧氏几何

我们提出 MechGeo，一种基于 Mathlib 的 agentic 框架，共同解决 Euclidean 几何中的忠实自动形式化和证伪证明构造问题。在 MechGeo 框架中，GeoFormalizer 代表在 GeoIR 中的不严谨问题，确定性地将其翻译成 Lean 4，并通过结构诊断和语义评估迭代地修复候选命题。GeoProver 构建几何证明计划，推导中间定理，并通过 Lean 中验证过的库选择性地代数化合适的子目标。Singular 或 SymPy 可生成代数证书，但所有生成的证明和反例均由 Lean 的核心检查。在七个不同的人工智能语言模型（LLM）后端上进行的实验结果显示，自动形式化有显著改进，特别是在模型直接翻译性能较弱的情况下。对于 43 个历史上的 IMO 几何问题，GeoFormalizer 生成了形式化的陈述，GeoProver 在 29 个问题中证明了这些陈述；对于剩余的 14 个问题，GeoFormalizer 生成了验证后的反例，并在专家修正后证明了所有修复后的命题。与 IMO 2026 问题 2 一起，这些结果展示了自动形式化和检查的 Lean 证明，形成了一个最大的报告中的 IMO 几何问题的自动、检查的 Lean 证明集合。在 LEAP 的 Lean-IMO-Bench 上，MechGeo 在 14 个几何陈述中首次证明了 12 个，正式反驳了剩余的两个，同时证明了所有修复后的命题。这些结果确立了反例引导诊断、几何推理和证伪符号计算作为可信的几何形式化基础。