有限单群分类定理完成 Lean 形式化， proofs 达 4310 万行

IgorCarron · x · 2026-10-28

Axiom Math 团队宣布完成「有限单群分类定理」（CFSG）在 Lean 中的完整形式化：总计 4310 万行 Lean 代码、205 万个声明、100 个里程碑，覆盖约 715 篇论文与书籍，每一步逻辑都经 Lean 内核校验。CFSG 第一代证明横跨数千页期刊、由约百位数学家历时数十年写成。

形式化过程中还发现已发表论文中的一处错误：通往 Unbalanced Group Theorem 的一个证明路线所用的闭包断言存在反例，团队已写出替代论证并发布论文，同时正与群论学者整理文献勘误。Tim Sweeney 感叹若 John Conway 在世看到这一幕该多好。