# AxiomMath 完成有限单群分类的 Lean 形式化

> 原标题：Classification of Finite Simple Groups Formalized in Lean

- 来源：Hacker News 首页
- 发布时间：2026-10-27T16:29:02.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/or0je6tkanx2kr979ntlso3fr
- 原文：https://cfsg.axiommath.ai/

## 摘要

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