Lean 4 完成有限单群分类形式化
Classification of Finite Simple Groups Formalized in Lean
有限单群分类定理是数学史上最宏大的集体成就，其初代证明横跨数千页期刊，由近百位数学家耗时数十年完成。如今，这一里程碑在 Lean 中实现了完整形式化，每一个逻辑步骤都经由 Lean 内核严格验证。项目团队在推进过程中，竟意外发现了一篇已发表论文中关于 Unbalanced Group Theorem 论证的漏洞，并提供了替代证明路径。这项工程汇聚了 4310 万行 Lean 代码和 205 万个声明，由 715 篇论文和书籍支撑，70 多位核心贡献者共同完成。这不仅是对数学真理的数字化重构，更是形式化验证领域的重大突破。
有限单群分类定理是数学史上最伟大的集体成就之一。
HN 评论区
42- Davidzheng
看到同伦基础论的拥趸们始终没能把事儿理顺，如今形式化已经如此成熟，却依然建立在集合论基础之上，这让我感到难过。
- mlmonkey
出于好奇：是否可以将一个前沿模型释放到所有数学教科书中，将每一个证明、定理、引理等全部转换为 Lean？前沿模型应该能做到这一点，对吧？而且这是一次性任务：做一次就一劳永逸，作为库永久存在，供其他证明使用。
也许我对 Lean 的理解有误；我把它看作是一种用于数学的编程语言。
- sebzim4500
这似乎是自动形式化的一个绝佳应用场景，因为过去数学家们曾错误地认为分类工作已经完成，结果却发现了缺失的类或散在群。
最初的证明是约 100 位数学家合作完成的，如果陶哲轩的说法正确，那么我们应该期待未来看到更多此类合作，就像我们在物理学中常见的那样。
- compacct27
群论是我进入抽象代数领域的入门药。一位朋友让我意识到对称无处不在，而群正是对称的形式化表达，理解这一切的旅程简直疯狂。前沿模型可以将这些抽象概念与通俗的英文示例联系起来，并能相当不错地回答问题，现在绝对是独自探索这个领域、看看它能为我们带来什么的最好时机。
- sleepyams
不知为何，有限单群分类总让我作为一名数学家感到不安，不过我想这有助于平息这种情绪。