AI写下近百万行代码，挑战核验规模庞大的数学证明工程
AI写下近百万行代码，挑战核验规模庞大的数学证明工程
借助人工智能（AI），数学史上规模最庞大的证明工程之一 ——有限单群分类（CFSG），正迎来一次前所未有的系统性核验。
近日，在清华大学讲席教授丘成桐的倡导下，清华大学求真书院领军班聂天骄、张傲、汤瑀森，丘成桐数学科学中心副教授周源、智能产业研究院副研究员李鹏以及华威大学副教授Damiano Testa组成团队，提出了AI辅助形式化证明工作流FormaTheoria，这套工具直接从原始零散文献切入，自动梳理知识点依赖关系、整合碎片化数学体系，再通过形式化证明助手完成严谨核验。截至2026年8月，它已完成4个关键定理的形式化证明，产出超99.4万行相关联的代码化数学理论，成为通往CFSG完整机器验证的重要里程碑。
FormaTheoria 的整体工作流：从文献检索、翻译和证明，到独立审查、协调修复与人工判断。 受访者供图
难以验证的“积木清单”
如果把所有数学运算结构想象成无数复杂的“几何体”，那么有限单群就是组成“几何体”的最基础的最小单元“积木”。而有限单群分类则是一张“积木清单”，几乎所有复杂的代数问题，基本都建立在这套“积木清单”之上。
作为近现代数学的底层核心理论之一，CFSG支撑了大量重要数学结论，一旦它存在漏洞，大量下游数学成果都可能受到影响。正因如此，过去数十年里，有百余位数学家接力证明该“清单”，成果散落在数百篇论文与专著中，总篇幅接近两万页。
然而，整套证明跨越不同年代、不同作者，各文献符号、定义、默认条件不统一，其中一处重要证明缺口，时隔20余年才由数学家撰写两卷共1220页专著补齐，人工完整核验几乎难以实现。
AI工具使得完成核验工作得以可能。然而，目前，AI面对的大多是一道已经准备好的数学问题，包括题目、定义和工具等，AI只负责寻找证明、输出逻辑证明即可。FormaTheoria则是直接从原始数学文献出发，自动梳理知识依赖关系，整合分散的数学知识，最终生成可由证明助手核验的形式化代码。
在这个过程中，团队有效应对了四项核心技术挑战：事先无法得知需要查阅多少文献、不同来源文献难以统一和兼容、无法判断是否忠于原文、原始文献存在原生缺陷。
FormaTheoria还建立了一张可持续更新的“证明地图”——把大目标拆解为辅助定理，成功结果向上汇总，失败路径则被记录下以避免重复“踩坑”，使得整套证明在长周期的工作中保持连贯。
此外，FormaTheoria还实现了相互独立的任务并行运行且互不干扰，其中多个任务共同依赖的前置结论，只需计算一次；而对于可能影响全局的结果，则采取串行修改方式，以确保一致性，规避冲突。研究表明，这一策略与非并行运行的策略相比获得了4.2倍的加速效果。
由此，FormaTheoria形成了一套完整的工作链路——文献检索、递归补齐依赖、文献翻译、证明构造、形式化机器核验、独立审查、冲突协调。整个流程中，一旦遇到存疑内容，系统会暂停自动化处理，移交人工研判。
7个月完成超15人6年的工作量
自2026年1月22日首次提交代码至8月2日，FormaTheoria“跑通”了Bender–Suzuki定理的完整理论链条，且依次完成 Feit Thompson 奇数阶定理、Glauberman Z*定理、Brauer Suzuki 定理、Bender Suzuki 定理的形式化证明。四个定理前后承接，后序证明建立在前序定理的基础之上。
研究人员介绍，目前已经产出99.4万余行形式化代码、850余个代码文件，累计研读15部书籍论文，合计1037页文献，远超人类处理能力。
AI 大幅压缩了大型证明工程的时间成本。以 Bender Suzuki 定理为证明终点为例，FormaTheoria形成了包含30298个数学声明、186187 条依赖关系的证明网络，最长依赖链达 458 层，单次最长运行 9.17 天，历经数百次信息压缩维护庞大证明网络。数学家对Feit Thompson 定理进行形式化时，是由15人耗费6年时间完成的，而FormaTheoria 仅用 7 个月就超出上述工作量并继续向前推进。
周源表示，可以说，近百万行代码背后是一张盘根错节、紧密链接的证明网络。这项研究表明，AI智能体已经可以在机器核验和分层审查的合力作用下，持续推进大型、超长程的数学工程。
探索人机协作新模式
值得一提的是，数学文献通常面向领域内的研究者，作者在写作中会省略前文已述条件，或默认读者能识别不同定义间的等价关系。一些排版或符号错误，人工阅读时也往往能被自然忽略或修正。但FormaTheoria在逐条翻译形式化代码时，把每个定义、条件和推理步骤都写得清晰明确、毫不含糊。正是这种严格逐行核验，让原始文献中隐而不见的问题凸显出来。
基于这样的策略，系统解决了两份经典文献的定义冲突，修正了沿用多年的疏漏。此外，还精准定位符号错误、下标偏差、因子错位等细节问题，将过往依靠经验脑补的模糊细节，转化为可复核的客观记录。
周源指出，尽管目前距离完整的有限单群分类形式化验证仍有巨大距离，但该研究表明，人工智能已跳出“解题”的局限，具备知识建构的能力，可在数月尺度维护百万行级别形式化数学体系，跨大量文献追踪复杂依赖，构建连通的数学理论。
此外，这项工作提出了一套可迭代复用的数学基础设施，包括形式化代码记录每条结论的依赖、文献衔接方式、勘误记录。未来搭配检索、可视化工具，可帮助研究者理解CFSG 整体架构，辅助数学家发现新联系、新定理。
周源表示，通过盖工作，团队旨在探索一种面向AI时代的人机协作模式，人类负责确定值得研究的问题并作出关键判断，AI承担大规模搜索与推导，形式系统则确保每一个被接受的步骤都可以被重新检验。当一项证明庞大到任何个人都难以从头复核时，这三者结合的方式，或许将成为人类管理超大规模数学知识的一条全新路径。