MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
MechGeo 是一个 Mathlib 原生的 agentic 框架，用于欧几里得几何的自动形式化和证明。GeoFormalizer 将非正式问题表示为 GeoIR，并确定性地翻译成 Lean 4，通过结构诊断和语义评估迭代修复候选语句。GeoProver 构建证明计划，推导中间引理，并选择性地代数化子目标。Singular 或 SymPy 可生成代数证书，但所有证明和反例都由 Lean 内核检查。在七个 LLM 后端的实验中，自动形式化有显著改进。在 43 个历史 IMO 几何问题中，GeoFormalizer 生成了形式化陈述，GeoProver 证明了 29 个；其余 14 个构建了反例，并在专家修正后证明了所有修复的陈述。加上 IMO 2026 问题 2，这构成了最大的自动化、内核验证的证明集合。
发展脉络
- 首次出现MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4arXiv cs.AI
- 当前判断MechGeo 展示了 agentic 框架在数学定理证明领域的潜力，通过自动化形式化和证明，可能加速数学研究。其方法可扩展到其他数学领域，推动 AI 辅助数学的发展。同时，该框架对 LLM 后端的依赖表明，模型能力仍是关键因素，但框架设计可以弥补部分不足。Agent Pulse · 分析
MechGeo 是一个 Mathlib 原生的 agentic 框架，用于欧几里得几何的自动形式化和证明。GeoFormalizer 将非正式问题表示为 GeoIR，并确定性地翻译成 Lean 4，通过结构诊断和语义评估迭代修复候选语句。GeoProver 构建证明计划，推导中间引理，并选择性地代数化子目标。Singular 或 SymPy 可生成代数证书，但所有证明和反例都由 Lean 内核检查。在七个 LLM 后端的实验中，自动形式化有显著改进。在 43 个历史 IMO 几何问题中，GeoFormalizer 生成了形式化陈述，GeoProver 证明了 29 个；其余 14 个构建了反例，并在专家修正后证明了所有修复的陈述。加上 IMO 2026 问题 2，这构成了最大的自动化、内核验证的证明集合。
MechGeo 通过将形式化与证明分离，并利用 GeoIR 作为中间表示，实现了对较弱 LLM 的自动形式化改进。其迭代修复机制结合结构诊断和语义评估，提高了形式化准确性。GeoProver 的代数化策略和 Lean 内核验证确保了证明的可靠性。这表明，通过专门的框架和中间表示，可以提升 LLM 在数学形式化任务上的表现，即使模型直接翻译能力较弱。
MechGeo 展示了 agentic 框架在数学定理证明领域的潜力，通过自动化形式化和证明，可能加速数学研究。其方法可扩展到其他数学领域，推动 AI 辅助数学的发展。同时，该框架对 LLM 后端的依赖表明，模型能力仍是关键因素，但框架设计可以弥补部分不足。
MechGeo 作为开源框架，可能降低数学形式化的门槛，吸引更多研究者使用 Lean 4。其自动化能力可能减少人工证明的工作量，提高效率。对于依赖数学验证的行业（如形式化验证、安全关键系统），该技术可能带来成本节约和可靠性提升。
未来，MechGeo 可能扩展到更多数学领域，并集成更强大的 LLM 后端，进一步提升自动化证明能力。其方法可能被整合到 Mathlib 中，成为标准工具。此外，该框架的成功可能激励更多类似 agentic 框架的开发，推动 AI 在数学研究中的应用。