Axiom称智能体集群完成有限简单群分类证明
先了解这件事
AI 综述
2026年10月27日，Elvis Saravia发文称，Axiom Math使用AI智能体集群正式验证了有限简单群分类证明：内容约15,000页，由100多位数学家参与，转化为约5,000万行Lean代码，并在24天内完成验证。智能体通过GitHub认领任务、撰写证明、相互审查和合并工作，同时修正已发表证明中的数百处重要勘误。同日，Rohan Paul报道称，该项目在数学家引导下用24天完成约15,000页、约4,000万行Lean形式化证明；早先报道称此前写出正确的10,000行Lean证明仍需数周指导，此次规模约扩大4,000倍，Axiom将其归因于同时重建模型、harness与基础设施三层。报道未提供证明正确性的独立验证细节。
报道时间线
10月27日
- Axiom 用 AI 智能体集群重写有限简单群分类的 15,000 页形式化证明
Axiom 称，AI 智能体集群在数学家引导下用 24 天完成了有限简单群分类约 15,000 页、约 4,000 万行 Lean 的形式化证明。此前写出正确的 10,000 行 Lean 证明还需数周引导，此次规模约扩大 4,000 倍。Axiom 将这一变化归因于同时重建模型、harness 与基础设施三层。
- Axiom Math 使用智能体集群验证有限简单群分类证明
Axiom Math 使用智能体集群正式验证了有限简单群分类证明，这项工作约含 15000 页内容、由 100 多位数学家参与，现已转化为约 5000 万行 Lean 代码，并在 24 天内完成验证。智能体通过 GitHub 认领任务、撰写证明、相互审查并合并工作，同时修正了已发表证明中的数百处重要勘误。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。