Axiom 用 AI 智能体群完成有限单群分类定理的 Lean 形式化

Axiom Math 宣布用 AI 智能体群完成有限单群分类定理的 Lean 形式化，称这是该定理首个完整的机器校验版本。原证明横跨约1.5万页、500余篇论文，凝聚约100位数学家数十年的工作，常被称为对称性的元素周期表。