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