华人创办 AI 公司完成最长数学证明形式化验证 4310 万行代码开源

近一个月 AI 加速深入数学研究领域，AI 产出证明的可信性成为数学界亟待解决的问题，形式化验证是重要应对路径，可借助证明助手将推导转化为计算机可逐步骤核验的形式语言。AI 数学公司 Axiom 宣布其 AI 智能体在 Lean 中完成了人类史上篇幅最长的有限单群分类定理（CFSG）的完整形式化，该定理原始证明超 1.5 万页、分散在数百篇文献中，此前完整读懂全部论证的学者已日渐稀少。Axiom 团队依托现有数学库及此前国内相关项目积累的群论代码，将整套论证拆分后调度数十个 AI 智能体协同工作，历时 24 天写出约 4310 万行 Lean 代码并开源，过程中解决了里程碑划分过粗、代码校验效率低等诸多问题，还排查出大量文献笔误、数据错误与遗漏前提，甚至在一处关键论证中发现原公开证明的疏漏，联合相关领域资深数学家补全了可靠的替代论证路线。该形式化成果让这份长期靠集体记忆维系的巨型证明的所有推导环节都可追溯核验，既回应了学界对 AI 证明可信性的担忧，也为后续相关数学研究提供了可复用的基础模块，为数学领域的可靠性提供了新的支点，让数学家得以抽身聚焦提出核心问题、深化对证明的本质理解等更具创造性的工作。