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

MechGeo 是一个基于 Lean 4 的智能体框架，用于欧氏几何问题的自动形式化与证明。它包含 GeoFormalizer 和 GeoProver 两个组件，通过反例引导修复、代数化子目标和内核校验，在 43 道历史 IMO 几何题中形式化并证明 29 道，在 LEAP 基准上首次证明 12 道并推翻 2 道。

此前，几何定理的自动证明多依赖人工形式化或专用工具，难以保证端到端可信。MechGeo 首次将反例引导修复、几何推理与内核校验的符号计算结合，在 IMO 几何题上显著提升自动形式化成功率，尤其对翻译能力较弱的模型效果明显，为可验证形式化数学建立了实用基础。

MechGeo 采用 GeoFormalizer 将非正式问题表示为 GeoIR，再确定性翻译为 Lean 4，并通过结构诊断和语义评估迭代修复候选语句。GeoProver 生成证明计划，推导中间引理，并通过 Lean 验证的库选择性地代数化子目标。Singular 或 SymPy 生成代数证书，但所有证明和反例均经 Lean 内核检查，保证了可信性。

对形式化数学工具链而言，MechGeo 展示了将自动推理与内核校验结合的产品范式，可能降低几何问题形式化的门槛，加速数学库建设。对基于 LLM 的数学产品，其反例引导修复机制可提升模型输出正确性，但当前依赖 Lean 环境，集成成本较高，且主要针对欧氏几何领域。

• 构建面向数学教育或竞赛的自动化几何证明助手，集成 MechGeo 流程，提供可验证的解题步骤。
• 开发反例引导的 LLM 修复引擎，用于提升模型在数学推理任务中的输出可靠性。
• 将 GeoFormalizer 的翻译迭代机制推广到其他数学领域，如代数或数论，扩大形式化覆盖范围。

• MechGeo 在非欧氏几何或更复杂数学领域的效果如何？
• GeoFormalizer 对自然语言问题描述的歧义处理能力是否有局限？
• 其性能提升对计算资源或延迟的具体要求未在证据中量化。