#CFSG

据该条目，项目方宣布已在 Lean 中形式化有限单群分类（CFSG）。现有材料没有说明这次形式化覆盖了分类定理的哪些部分、依赖哪些公理，也没有给出可构建的代码或独立验证结果，因此目前应把它视为项目方公告，而非已经复核的完整证明。