热点事件持续更新
Axiom Math 称 AI Agent 完成有限单群分类定理 Lean 形式化
1 篇报道1 个报道来源5 小时前更新
先了解这件事
事件综述
2026 年 10 月 26 日，AI 数学公司 Axiom Math 宣布，由数十个 AI Agent 在 24 天内完成了有限单群分类定理（Enormous Theorem）的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，并称这是第一份覆盖整个分类定理的计算机检查证明。10 月 28 日，36氪对此进行了报道。目前该成果仅见于 Axiom Math 的宣布及媒体转述，尚无独立第三方核验或同行评议信息，事件处于公布后的待验证状态。
根据公开报道整理 · 5 小时前更新
最新进展10月28日 16:19
36氪 10 月 28 日报道 Axiom Math 上述宣布，暂无独立核验进展。报道时间线
沿着报道，了解事件的不同侧面。
10月28日
- 36氪公开报道Axiom Math 用数十个 AI Agent 在 24 天内完成有限单群分类定理的 Lean 形式化
AI 数学公司 Axiom Math 于 10 月 26 日宣布，由数十个 AI Agent 在 24 天内完成了有限单群分类定理（Enormous Theorem）的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，给出了第一份覆盖整个分类定理的计算机检查证明。
本事件热度走势
当前热度 9·可比范围峰值 10（10月28日 17:00）·近 24 小时可比范围变化 –
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。