Axiom 用 agent 蜂群把有限单群分类整个写进 Lean，顺手揪出教科书里 34 处偏差
有限单群分类定理被数学家叫做"巨型定理"不是没道理：证明散落在几百篇论文、几万页纸里，前后写了半个世纪。Axiom 刚把它完整形式化进了 Lean，大部分活是一群 agent 用三周半干完的。
项目页上的数字：4310 万行 Lean，205 万条声明，覆盖 715 篇论文和专著。第一批蜂群 10 月 2 日上线，agent 通过 GitHub issue 认领里程碑，牵头的 agent 负责拆解难的论证、审核要形式化的命题，每一步推导交给 Lean 检查。10 月 10 日团队发了一句"我们证明了魔群是单群"。公开仓库 10 月 27 日放出，过程中请了群论学者 Lyons 和 Solomon 把关。
真正值钱的不是规模。蜂群找出了已发表文献里 34 处值得注意的偏差，包括 Aschbacher 和 Smith 书里一条引理的反例，以及不平衡群定理证明中一个闭包断言的问题。人类核对了几十年的文献照样有洞，agent 在严格检查器底下把它们翻了出来。
坦白的部分同样有用。Axiom 承认 agent 有时"假设了而不是证明了"前置条件，团队因此删掉了"几万行建在这些假设上的代码"。agent 产出证明的速度还一度快过 Lean 重新检查的速度。所以这个月反复出现的那条结论又被验证一次：蜂群负责产量，验证器负责真假，人的活缩到只剩确认顶层命题和定义说的是你想说的东西。
项目页：https://cfsg.axiommath.ai/ 博客：https://axiommath.ai/research/the-enormous-theorem-formalized/ 仓库：https://github.com/AxiomMath/CFSG
← 返回所有文章
项目页上的数字：4310 万行 Lean，205 万条声明，覆盖 715 篇论文和专著。第一批蜂群 10 月 2 日上线，agent 通过 GitHub issue 认领里程碑，牵头的 agent 负责拆解难的论证、审核要形式化的命题，每一步推导交给 Lean 检查。10 月 10 日团队发了一句"我们证明了魔群是单群"。公开仓库 10 月 27 日放出，过程中请了群论学者 Lyons 和 Solomon 把关。
真正值钱的不是规模。蜂群找出了已发表文献里 34 处值得注意的偏差，包括 Aschbacher 和 Smith 书里一条引理的反例，以及不平衡群定理证明中一个闭包断言的问题。人类核对了几十年的文献照样有洞，agent 在严格检查器底下把它们翻了出来。
坦白的部分同样有用。Axiom 承认 agent 有时"假设了而不是证明了"前置条件，团队因此删掉了"几万行建在这些假设上的代码"。agent 产出证明的速度还一度快过 Lean 重新检查的速度。所以这个月反复出现的那条结论又被验证一次：蜂群负责产量，验证器负责真假，人的活缩到只剩确认顶层命题和定义说的是你想说的东西。
项目页：https://cfsg.axiommath.ai/ 博客：https://axiommath.ai/research/the-enormous-theorem-formalized/ 仓库：https://github.com/AxiomMath/CFSG
评论