RecodeX 重构消息，数学博客John D. Cook发文指出，有限单群分类定理（CFSG）被称为数学界规模最大的定理，其证明历经数十年、累计数千页期刊论文。两天前，Axiom宣布已完成该定理证明的形式化验证。