Axiom Math 用数十个 Agent 在 24 天内完成有限单群分类定理 Lean 形式化
数十agent，24天挑战数学界巨型工程，还揪出40年前漏洞
AI 导读
Axiom Math 宣布，由 AxiomProver 协调的数十个 AI Agent 在 24 天内完成有限单群分类定理的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，项目已上传 GitHub 且最终证明不含 sorry。
推荐理由
文章梳理了数十个 Agent 24 天形式化有限单群分类定理的工程细节，读者可以了解 AI 参与大规模数学证明的协作方式与实际障碍。
来源：机器之心 · mp.weixin.qq.com