Axiom 用 Agent 集群 24 天完成 CFSG 的 Lean 形式化
- 核心发布：Axiom 宣布完成有限单群分类（CFSG）的完整 Lean 形式化。原始证明约 15,000 页、分散在约 500 篇论文中，由 100 多位数学家完成。
- 过程与规模：Agent 集群在 24 天内产出约 5000 万行 Lean 代码；Agent 认领任务、互相审查并通过 GitHub 合并，人类提供指导，过程中报告修复了数百处已发表证明中的勘误。
- 记录与边界：研究者指出，这取代四色定理成为最大的计算机验证证明；能完整理解 CFSG 证明的人极少，形式化能检查证明步骤，但不等同于数学界对结果重要性与正确性的全面确认。
- 行业观察：多 Agent 协作、任务认领与互相审查被用于超大规模形式化工程，验证成本从人工逐行审阅转向机器检查与社区消化；对需要构建可信数学库或形式化规范的团队，这是一条可复用的工程路径。 🔗 Axiom 公告 | AINews