MechGeo：首次在 Lean 4 中大规模完成IMO 

几何题自动形式化与机器证明

从自然语言题目到可由 Lean 内核独立核验的完整证明

核心成果：MechGeo 对 2000—2026 年 44 道 IMO 几何题构造了忠实形式化与完整 Lean 证明。据作者所知，这是目前公开报道中规模最大的自动化、经通用证明助手内核核验的 IMO 几何证明集合。

    近日，中国科学院数学与系统科学研究院支丽红研究员、沈皓（博士生）和肖羽轩（硕士生），与中山大学郭俊余（硕士生）、山东大学崔添（本科生）共同提出了可信几何推理框架 MechGeo。该系统基于 Lean 4 及其大型数学库 Mathlib，将自然语言几何问题的自动形式化、命题诊断、证明构造与反例验证整合到统一的验证闭环中。

    20 世纪 70 年代末，吴文俊先生提出以特征列为核心的“吴方法”，把初等几何命题转化为多项式问题并实现机械化证明，开创了数学机械化的重要方向。此后，高小山、周咸青、张景中等进一步发展几何不变量、可读证明生成和演绎数据库方法，持续推动机器证明从代数判定走向更短、更接近传统几何语言的证明。

    MechGeo 延续了这一学术脉络。其名称取自“mechanized geometry”，也寄托着对吴文俊先生在几何定理机器证明领域奠基性贡献的纪念。系统进一步将大语言模型、计算机代数与通用证明助手相结合，使自动生成的证明能够由 Lean 内核独立复核。

    GeoFormalizer先用中间语言 GeoIR 表达题目的对象、构造与几何关系，再按固定规则确定性地翻译为 Mathlib 原生的 Lean 4 命题。静态检查、Lean 编译与语义评估共同发现类型错误、结构缺失及语义偏差，并指导迭代修复。

    GeoProver根据形式化命题规划证明、提出中间引理，并只对合适的子目标进行代数化。Singular 或 SymPy 可以生成代数证书，但证书、反例和最终证明都必须在 Lean 中重建并通过内核检查。

图 1 MechGeo 总体框架：形式化、证明、反例与独立核验形成闭环

    43 道历史IMO 几何题：GeoProver 直接证明了GeoFormalizer 自动生成的29 个忠实命题；对其余14 个命题，系统构造出经Lean 验证的反例，揭示缺失的非退化条件或点序条件。经专家据此修复后，14 个修复命题全部得到证明。

    IMO 2026 第 2 题：系统从原始自然语言表述出发，直接完成形式化和完整证明。由此，2000—2026 年的 44 道题均形成了忠实、可复现且经 Lean 内核核验的证明。

    Lean-IMO-Bench：在Google DeepMind 的LEAP 基准所含14 道几何题中，MechGeo 首次证明了12 个原始Lean 命题，并形式化反驳另外2 个存在条件缺失的命题。补充必要条件后，两个修复版本也均被证明。Google DeepMind 随后在公开的 IMOBench 仓库中确认并致谢了 MechGeo 团队对这两处形式化问题的发现和修正。

论文：MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

基准与代码：MechGeoBench

基准修正记录：Google DeepMind IMOBench

作者：沈皓*、郭俊余*、崔添、肖羽轩、支丽红†（*共同第一作者，†通讯作者）。

合作单位：中国科学院数学与系统科学研究院、中山大学、山东大学。

项目支持：国家重点研发计划（2023YFA1009401）和中国科学院战略性先导科技专项（XDA0480501）。