据该条目，项目方宣布已在 Lean 中形式化有限单群分类（CFSG）。现有材料没有说明这次形式化覆盖了分类定理的哪些部分、依赖哪些公理，也没有给出可构建的代码或独立验证结果，因此目前应把它视为项目方公告，而非已经复核的完整证明。
背景
有限单群分类（CFSG）是有限群论的核心定理，其第一代证明篇幅巨大、分散在大量文献中；一篇介绍性报道称原证明约有 1.5 万页。Lean 是带内核检查器的定理证明器，形式化要求把定义、引理和证明步骤写成 Lean 能接受的形式，并由内核逐项验证；Axiom Math 的发布页称此次工作完整覆盖了 CFSG 的第一代证明。
参考链接
社区讨论
对 Lean 用户而言，实际影响取决于该形式化是否提供可构建、可导入的代码以及其公理依赖；在这些信息公布前，不能把它直接当作可替代文献证明的库依赖。
有评论者对形式化仍基于集合论基础、而非同伦类型论表示遗憾；另一条评论则认为自动形式化对 CFSG 特别有用，因为历史上曾出现误以为分类完成、后来才发现遗漏类或散在群的情况，并提到原证明由约百名数学家合作完成。