数十 AI Agent24 天完成数学巨型工程 揪出 40 年前论证漏洞

数十个 AI Agent 仅用 24 天就完成了人类上百位顶尖数学家耗费数十年、分散在 500 多篇论文中的有限单群分类定理的 Lean 形式化，生成约 4310 万行可由计算机逐步验证的代码与 205 万个形式化声明，产出了首份覆盖整个分类定理的计算机检查证明。形式化过程中，AI 不仅排查出 34 处文献偏差，揪出了该定理相关研究中存在近 40 年的论证漏洞，还参与构造了新的群论结果。整套形式化成果完全依托标准公理，无未完成证明的占位符，已全部公开，将原本零散的数学推理整合为可机械化核验、追踪溯源、复用扩展的完整形式系统，大幅降低了过往引用该巨型定理时追溯数百篇关联文献的核查难度。