Classification of Finite Simple Groups Formalized in Lean

AxiomMath 公布有限单群分类的完整 Lean 形式化，沿用第一代证明路线，每个逻辑步骤均由 Lean 内核检查。项目包含 43.1M 行 Lean 代码、2.05M 项声明，覆盖 715 篇论文及书籍。