MechGeo：在 Lean 4 中自动形式化并证明欧氏几何
原标题:MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
AI 导读
MechGeo 是原生集成 Mathlib 的智能体框架，联合处理欧氏几何题的忠实形式化与内核认证证明。GeoFormalizer 将自然语言转为 GeoIR 和 Lean 4，并通过结构诊断、语义评估迭代修复；GeoProver 规划证明、生成引理并选择性代数化子目标。43 道历史 IMO 几何题中，29 道被证明，14 道被 Lean 核验为反例并在专家修正后全部证明；Lean-IMO-Bench 的 14 题中证明 12 道并形式反驳 2 道。
为什么值得读
几何自动定理证明的关键瓶颈从“生成证明”扩展到“发现错误命题”，该工作用 Lean 内核同时核验证明、反例与修正版结果。
深度解读
发生了什么
原始事实： 论文提出 MechGeo，一个基于 Mathlib 的 Lean 4 智能体框架，目标是自动形式化并证明欧氏几何问题。系统由 GeoFormalizer 与 GeoProver 两部分组成，并报告了历史 IMO 几何题、IMO 2026 Problem 2 及 LEAP Lean-IMO-Bench 几何题上的结果。
核心技术
原始事实： GeoFormalizer 先将非形式化题面表示为 GeoIR，再确定性地翻译为 Lean 4；它利用结构诊断和语义评估迭代修复候选命题。GeoProver 生成几何证明计划、推导中间引理，并把适合的子目标转化为代数问题。Singular 或 SymPy 可以生成代数证书，但最终证明与反例均由 Lean 内核检查。
关键证据与数字
原始事实： 实验覆盖 7 个 LLM backbone。43 道历史 IMO 几何题中，GeoFormalizer 生成的形式命题有 29 道被 GeoProver 证明；其余 14 道产生了 Lean 核验的反例，专家修正后全部被证明。LEAP 的 Lean-IMO-Bench 几何子集包含 14 题，其中 12 题首次被 MechGeo 证明，另外 2 题被形式反驳，修正版本也均被证明。
为什么重要
分析： 形式化系统的失败不只来自证明搜索，也可能来自自然语言到形式命题的语义偏差。MechGeo 把反例作为诊断信号，使系统能够区分“原命题可证”“原命题不成立”和“修正后可证”。这为评估 LLM 数学推理提供了比单纯证明成功率更完整的指标。
实际影响
分析： 对 Lean 数学库建设而言，GeoIR、几何引理生成和选择性代数化可能降低人工形式化成本。对自动定理证明评测而言，报告反例及修正版证明有助于识别基准题面或形式翻译中的错误。工程上，所有外部计算器输出都必须经过 Lean 内核复核，因而更适合用于可审计的证明流水线。
局限与不确定性
原始事实与不确定性： 摘要没有给出 7 个 backbone 的具体名称、各阶段单独成功率、运行成本、证明长度或与基线的完整对比，也未说明 14 个修正版由专家如何确定。摘要中的“最大报告集合”是作者在限定范围内的表述，仍需正文和相关工作核对。论文还未在此处提供不同几何表示、复杂度分布或对 GeoIR 错误的系统消融结果，因此不能仅凭摘要判断方法对新题型的泛化能力。
原始来源
- arXiv 摘要页
- 论文标题：MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
- arXiv ID：2608.02295