Axiom Math 用数十个 AI Agent 在 24 天完成有限单群分类定理 Lean 形式化，生成约 4310 万行代码并发现 40 年前的论证漏洞
数十agent，24天挑战数学界巨型工程，还揪出40年前漏洞
AI 导读
Axiom Math 于 10 月 26 日宣布，由数十个 AI Agent 在 24 天内完成有限单群分类定理（巨型定理）的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，并已在 GitHub 公开。
推荐理由
原文详述了数十个 AI Agent 在 24 天内形式化有限单群分类定理的协作流程与踩坑细节，读者可以了解大规模 Agent 工程的任务拆解和验证方法。