人类史上最大数学证明完成 Lean 形式化:4310 万行代码逐条机器验证

pickover · x · 2026-10-28

有限单群分类(CFSG)的第一代证明在 Lean 中完成完整形式化,由 Lean kernel 逐条逻辑验证,被称为人类史上最大的数学证明——原证明横跨数千页期刊论文,由约百名数学家历时数十年写成,证明每个有限单群都是素数阶循环群、交错群、李型群或 26 个零散群之一。

项目规模:4310 万行 Lean 代码、205 万条声明、100 个里程碑、覆盖 715 篇论文与书籍。过程中还发现已发表的 Unbalanced Group Theorem 论证路径存在反例问题,并基于 Solomon 1976 年极大 2-分量理论给出替代证明,产出一篇 35 页新论文;团队正与群论学者整理文献勘误。