Axiom 24 天用 AI agent 集群形式化「巨大定理」，产出 4300 万行 Lean 代码
rohanpaul_ai · x · 2026-10-27
Axiom Math 宣布完成有限单群分类定理（CFSG）的首个完整计算机校验证明，这是数学史上最长的证明：原证明横跨约 15000 页、500 多篇论文、约 100 位数学家参与，人称「巨大定理」（相关工作者 John Thompson 曾获菲尔兹奖与阿贝尔奖）。
关键事实：
- 团队用 24 天时间，调度数十个 AI agent 组成的集群，在 Lean 证明助手中产出约 4310 万行代码。
- CFSG 给出有限群的「原子」——有限单群的完整分类，被誉为有限对称性的元素周期表。
- 这是 Lean 形式化与 AI agent 大规模协作在数学前沿的一次标志性落地。
所属事件:Axiom 完成 1.5 万页有限单群分类定理 Lean 形式化(11 条相关)→
「漫话AGI」频道最新
- After42：专家认定 AI 提出的 135 个研究问题中 45 个真有趣 — james_y_zou · 2026-10-28
- Mantic 预测:开源模型 9 个月内将具备 Astra 级攻击性网络能力 — tshevl · 2026-10-28
- Mantic 预测：开源模型距前沿级攻击性网络能力仅差约 9 个月 — tshevl · 2026-10-28
- 观点交锋：从 AI 获益最多的，是知道「什么是好工作」的人 — brandon_galang · 2026-10-28
- Juan Benet 创立 PLC Neurotech 基金:神经科技正处 AI 2019 年时刻 — juanbenet · 2026-10-28
- AI 圈争论：把智力生活归功于 AI 公司机械化，是厌人症吗 — wfithian · 2026-10-28