有限单群分类定理完成 Lean 形式化
Axiom Math 团队宣布完成有限单群分类定理（CFSG）第一代证明的完整 Lean 形式化，每个逻辑步骤均由 Lean kernel 检查。项目规模约 4310 万行代码、205 万条声明，覆盖 715 篇论文与书籍、100 个里程碑。形式化过程中还审查出已发表论文中的多处证明问题，其中一处据称得到修正。
2026-11-03 ~ 2026-11-03 · 2 条相关
- 第 1 集:Axiom 用 AI 智能体 24 天 Lean 形式化有限单群分类定理(2026-10-27,34 条)
- 第 2 集:有限单群分类定理完成 Lean 形式化(2026-11-03,2 条)
- 有限单群分类定理完成 Lean 形式化：4310 万行代码，还揪出已发表论文的一处证明问题 — ChrSzegedy · 2026-11-03
- 有限单群分类定理完成 Lean 形式化，4300万行代码揪出47篇论文96处错误 — ChrSzegedy · 2026-11-03