先了解这件事
2026年10月27日,Axiom Math发布其称为首个完整计算机检验的有限单群分类(CFSG)证明。据Unite.AI报道,该项目由工程师和数学家指挥数十个AI智能体,在24天内写出约4310万行Lean代码;项目页列出205万条声明、715篇论文与书籍语料,代码为不含sorry的Lean4证明,固定版本4.35.0-rc3,基于Mathlib和TauCeti,采用Apache-2.0许可。凤凰科技同日报道称,过程中智能体发现34处文献偏差,包括1986年John Walter不平衡群定理研究中的一处闭包断言反例,并参与构造并形式化新结果“Preservation of simple tops”,写入35页论文作为定理2.3。项目已上传GitHub,声明最终证明不含sorry、仅依赖标准公理,仓库审查状态为团队自评。
AI 根据公开报道生成
事件进展
1 个已确认进展
- 来源：Unite.AI
报道与讨论时间线
按时间查看正式报道与传播讨论；两类内容的证据等级保持独立。
10月28日
Testing Catalog
Axiom 开源仓库：数十个 AI 智能体 24 天生成约 4300 万行 Lean 代码
Axiom 发布一个开源 GitHub 仓库，数十个 AI 智能体在 24 天内把 1.5 万页的有限单群分类证明转成约 4300 万行代码。代码用 Lean 编写，可逐步校验证明，整个结果通过运行代码验证而非重读数百篇论文。Axiom 的图表追踪 2025 年年中以来 AI 编写的 Lean 项目规模，按其估算约每 37 天翻一倍。
凤凰科技精选
Axiom Math 用数十个 Agent 24 天形式化有限单群分类定理，生成 4310 万行 Lean 代码
Axiom Math 宣布，由人类数学家和工程师组织的数十个 AI Agent 在 24 天内完成了有限单群分类定理的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，覆盖 715 篇参考文献。过程中 Agent 发现 34 处文献偏差，包括 1986 年 John Walter 不平衡群定理研究中的一处闭包断言反例，并参与构造并形式化了新结果「Preservation of simple tops」，写入 35 页论文作为定理 2.3。项目已上传 GitHub，声明最终证明不含 sorry，仅依赖标准公理，仓库审查状态为团队自评。
阿易 AI Notes
Axiom 称 AxiomProver 智能体群 24 天完成有限单群分类定理 Lean 形式化
Axiom 宣布完成有限单群分类定理的完整 Lean 自动形式化，该证明约 15000 页、由 100 多位数学家跨代完成。据转述，AxiomProver 智能体群用 24 天产出约 5000 万行 Lean 代码，并修复了原著中的逻辑漏洞。
Rohan Paul
Axiom 智能体集群用 24 天形式化验证有限单群分类证明
Axiom 的 AI 智能体集群用 24 天完成了有限单群分类（CFSG）证明的逐步验证，将 500 多篇论文、约 15000 页内容转成 3800 万行以上机器可验证代码，并发现已发表记录中 34 处严重不一致。该证明此前 40 多年无人能独自完整核验。
Unite.AI精选
Axiom Math 发布 4310 万行 Lean 有限单群分类形式化证明
Axiom Math 于 2026 年 10 月 27 日发布其称为首个完整计算机检验的有限单群分类（CFSG）证明，由工程师和数学家指挥数十个 AI 智能体在 24 天内写出约 4310 万行 Lean 代码。项目页列出 205 万条声明、715 篇论文与书籍语料，代码为 sorry-free 的 Lean4 证明，固定版本 4.35.0-rc3，基于 Mathlib 和 TauCeti，采用 Apache-2.0 许可。Axiom 称形式化过程中发现公开证明的 34 处值得注意的偏差，最实质的一处涉及 Unbalanced Group Theorem，并称 AxiomProver 产出了新定理 Theorem 2.3 用于修补。
10月27日
Rohan Paul
Axiom 用 AI 智能体集群 24 天完成 15000 页数学证明的 Lean 形式化
Axiom 宣布完成有限单群分类的 Lean 自动形式化，这份数学证明约 15000 页、由 100 多位数学家跨代完成，改写后约 4000 万行 Lean 代码，由 AI 智能体集群在数学家引导下用 24 天写出。Axiom 称今年年初让 AxiomProver 写出正确的 1 万行 Lean 证明还需数周反复引导，此次规模约为其 4000 倍，并将跃升归因于同时重建模型、harness 和基础设施三层。
本事件热度走势
- 当前
- 43
- 区间峰值
- 49 10月28日 11:00
- 近 24 小时变化
- —
移动指针或点击图表可查看每小时热度；键盘可用左右方向键切换。