Axiom 称 AI 智能体 24 天形式化有限单群分类定理
热点事件持续更新
Axiom 称 AI 智能体 24 天形式化有限单群分类定理
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
Axiom 宣布用 AI 智能体在 24 天内完成了有限单群分类定理的首次完整 Lean 形式化，生成约 4000 万行代码。该定理原证明约 1.5 万页、依赖 500 多篇论文、约 100 位数学家参与，被视为最长的数学证明。 完成情况和“首次完整”的定性均出自 Axiom 的公布，尚无独立验证信息。
AI 根据报道生成 · 2 小时前更新
最新进展10月27日 23:12
Axiom 用 AI 智能体在 24 天完成有限单群分类定理的 Lean 形式化报道时间线
沿着报道，了解事件的不同侧面。
10月27日
- Rohan PaulAxiom 用 AI 智能体在 24 天完成有限单群分类定理的 Lean 形式化
Axiom 宣布完成有限单群分类定理（CFSG）的首个完整计算机验证证明，用约 4000 万行 Lean 代码形式化了这部约 15000 页、500 多篇论文、约 100 位数学家参与的最长数学证明。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。