史上最大数学证明获 Lean 全自动形式化:有限单群分类 1.5 万页

PlisSergey · x · 2026-10-28

Axiom 宣布完成对「有限单群分类定理」的完整 Lean 自动形式化——这是人类历史上最大的数学证明,约 15,000 页,由 100 多位数学家跨越数代人合作完成,被称为「对称性的元素周期表」。

转发的评论者(一位数学家)据此提出:不做自动形式化的数学家,将像坚持手写每一行代码的程序员一样陷入自我安慰。他分享亲身经历:花约 5 小时学会读 Lean 并搭建 autoformalization 环境后,自己的旧论文已全部完成机器验证;细小错误被自动抓出;可以快速验证模糊想法是否可行,也能不经等待同行评审就确认他人新结果是否可靠。「不明白现在还有谁愿意在没有这个工具的情况下做数学。」