有限单群分类（CFSG）被认为是数学史上最重要的集体成就之一。该定理指出，每一个有限单群——有限群论的基本构建块——都属于几个类别之一：素数阶循环群、交错群、李群（Lie type groups）或 26 个“奇异”群之一。由于原始证明是一项跨越数十年、涉及约 100 名数学家并分布在数千页期刊文章中的庞大工程，它长期以来一直是形式化验证的候选对象，旨在确保其绝对的逻辑完整性。
这张图片代表了使用 Lean 定理证明器形式化有限单群分类的总体项目。
AxiomMath 的研究人员现在已在 Lean 中完成了 CFSG 的完整形式化。Lean 是一种用于验证数学证明的功能式编程语言和交互式定理证明器。该项目遵循 CFSG 的“第一代”证明，确保每一个逻辑步骤都经过 Lean 内核的检查。该形式化是“无 sorry”的，这意味着它不依赖于未证明步骤的占位符。团队利用 TauCeti 项目的 CFSG 陈述作为基准，并在 Mathlib 和 TauCeti 之上构建证明，使用了 `Classical.choice`、`propext` 和 `Quot.sound` 等标准公理。
该形式化项目最重要的成果之一是发现了现有文献中的一个技术错误。在验证第一代证明的过程中，团队发现了一个用于通往不平衡群定理（Unbalanced Group Theorem）的已发表路径中闭包断言的反例。为了解决这个问题，团队基于 Solomon 1976 年关于极大 2-分量的理论，为单群情况开发了一种替代论证。这一发现突显了形式化验证的效用：通过将人类编写的证明转换为机器可检查的代码，研究人员可以揭示复杂的多作者数学作品中细微的漏洞，而这些漏洞在其他情况下可能会被忽略多年。该项目目前包含超过 4300 万行 Lean 代码，并包含一个交互式证明图，用于可视化语料库中各种论文和书籍之间的依赖关系。
这张图片与项目的庞大规模以及托管形式化的仓库有关。