有限单群分类(CFSG)在现代数学中,堪称规模最为庞大的证明工程之一。
这项证明,由上百位数学家耗时数十年接力完成,其成果散落在数百篇论文与专著之中,总篇幅接近两万页,体量已经远远超出单人甚至单个团队能够完整复核的边界。
在这样的背景下,引入AI辅助进行大规模形式化验证,成为一条必须尝试的新路径。
为推动AI for Math的发展,在丘成桐先生的倡导下,来自清华大学求真书院领军班学生,以及丘成桐数学科学中心、智能产业研究院和华威大学的研究团队,提出了FormaTheoria——数学研究人工智能辅助工作流:让AI从原始数学文献出发,自动梳理依赖关系、整合知识体系并构建形式化证明,最后交由Lean证明助手逐步核验。
截至2026年8月,FormaTheoria已经完成四个关键定理的Lean形式化,产出超过99.4万行相互关联的代码化数学理论。虽然距离完整验证有限单群分类仍有很长一段路,但这一成果已经成为通往这一最终目标的重要里程碑。
CFSG为大量重要数学成果提供底层系统
“有限单群分类”听起来十分抽象。通俗地说,它就像一张关于有限对称性的“基本零件清单”:任何一个复杂的有限对称结构,都可以被层层拆解,最终得到一批无法继续拆分的基本单元;而CFSG的作用,就是告诉数学家这些基本单元究竟有哪些。
通常,数学研究会率先把一个复杂的问题拆到这些基本单元上,然后依据CFSG提供的完整清单逐类处理。因此,CFSG成为其他证明可以随时调用的基础设施。如果这套“基础设施”隐藏漏洞,那么建立在其相关结论之上的大量后续成果都可能受到影响。
一些专业综述为GFSG的应用提供了量化证明。美国数学会在2018年专门出版了Stephen D. Smith的专著“Applying the Classification of Finite Simple Groups: A User’s Guide”,全书231页、共10章,梳理了GFSG的应用场景。书中最后两章的公开目录列出14个带有编号的应用专题,包括距离传递图、Frobenius猜想、置换群算法、有限生成群的子群增长、域扩张、黎曼曲面覆盖、群论中的Waring问题、扩展图与近似群等。
GFSG的应用价值也得到了国际数学界最高层级的认可。2014年国际数学家大会邀请美国数学会2018年Cole代数学奖得主Robert Guralnick作题为“Applications of the Classification of Finite Simple Groups”的专题报告。
这些应用中包括极具学术影响力的重要成果。CFSG是限制Burnside问题完整证明链中的关键环节,Efim Zelmanov因解决这一问题获得1994年菲尔兹奖。Smith的专著还将有限单群上的Waring问题和扩展图等方向列为CFSG的重要应用方向,相关代表性论文发表于《Annals of Mathematics》(Waring问题;有限单群的直径及其应用)。这些例子表明,CFSG已经支撑起一系列斩获顶级学术奖项并登上数学顶级期刊的重要工作。
从这个意义来看,CFSG已经成为一套被反复使用的底层系统。随着下游成果越积越多,验证其正确性及可复核性,就变得愈发关键。对CFSG进行可追踪、可重复的机器核验,具有了超出群论本身的意义。
然而,其中困难在于,这套底层系统的证明来自不同年代、不同作者和不同文献,使用的符号、定义和默认条件常常不一致,一条引用甚至可能指向另一整套文献。历史上,分类证明中的一个重要缺口,直到二十多年后才由两卷、多达1220页的专著补齐。FormaTheoria不仅需要逐步核验单步推理,还要检查数百篇文献之间的定义、条件和引用能否完整衔接,最终形成一条没有断点的证明链。
AI如何推进超大规模证明工程
许多AI数学系统面对的是一道已经准备好的题目,包括题目、定义和工具全部准备就绪,AI只负责寻找证明。但FormaTheoria不一样,它需要先从一堆零散的文献中,重建题目背后的数学基础,再完成证明。这项工作主要面临四个难点:
第一,系统事先不知道需要查阅多少资料。
一条引用可能牵出另一篇论文,那篇论文又会引出更多前置工作。项目最初只有3个主要来源,证明过程中又发现了12个来源;后来补充的材料占全部查阅页码的65.6%。FormaTheoria的处理方法是:一旦发现缺失某个前置定理,就会暂停当前证明,查找并形式化这一依赖项,再回到原任务继续推进。已经完成核验的结果,会存进统一的知识库中,供后续证明反复调取。
第二,不同文献之间很难直接拼接。
不同作者使用不同的定义、符号和默认条件。两个定义在数学上可能完全等价,但一旦写进Lean代码,却可能互不兼容。FormaTheoria会反复比照原文和已有代码,搭建起必要的转换关系。同时,系统会保护已经核验过的数学陈述,并检查每一处修复是否会影响后续证明。这样一来,多本各自独立的著作和论文,才能够逐步融入同一套理论框架。
第三,代码通过检查仍可能误解原文。
Lean只负责检查证明逻辑是否自洽、结论是否由前提推出,却无法评判这个结论是否忠实于原文。AI很可能遗漏某个条件、混淆“所有”和“存在”,甚至错误地改动了结论。为此,FormaTheoria专门设置了独立的审查关卡:翻译组件率先写出Lean陈述,审查组件再对照原文逐项核对。在论文分析的14个文献小节中,11个小节的首轮翻译都被退回修改。这一独立审查机制,由此成为机器核验之外的第二道“保险”。
第四,原始文献本身也可能存在问题。
旧文献中可能出现排版错误、条件缺失或表述含混。FormaTheoria会保留原始页面,待后续证明遇到矛盾时,再回溯追查。如果文献能够支持修正,系统就补充条件或建立兼容关系;如证据不足时,系统会记录问题并交给数学专业人员判断。
除此之外,这项工程还要求AI在漫长的周期内保持节奏。一次对话无法容纳完整任务。为此,FormaTheoria采用一张持续更新的“证明地图”来管理进度:较为艰巨的目标被拆成较小的辅助定理,成功的结果逐层汇回主定理,失败路线也会被记录下来,避免系统反复走入同一条死胡同。
在并行策略上,项目也有特殊设计。相互独立的任务可以同时推进;多个任务如遇到同一个前置结果时,系统只完成一次,并允许其他任务复用。而那些可能牵一发动全身的公共数学内容,则按顺序逐个修改,避免冲突。论文的对照实验显示,这种依赖感知的并行方式,在所测试任务上实现了4.2倍加速。
FormaTheoria由此形成了一条完整工作链:寻找文献、补齐依赖、翻译原文、构造证明、机器核验、独立审查、协调冲突,并将拿不准的问题交给数学专业人员。每一步都责任明确、有据可查。这恰恰是针对超大规模证明工程中实际出现的困难,而做出的设计,赋能AI将分散的数学文献逐步连接成一套可检查、可追踪、可持续扩展的理论体系。
△
七个月,四个关键定理,近百万行可核验代码
2026年1月22日,FormaTheoria首次提交代码,至2026年8月2日,项目已经打通了一条延伸至Bender–Suzuki定理的关键理论链条,中间还依次完成了Feit–Thompson奇数阶定理、Glauberman Z*定理和Brauer–Suzuki定理的证明。
这四个定理并非彼此孤立,他们构成了有限单群分类中的一条相互衔接的重要路线,后一个定理的证明往往建立在前者奠定的庞大数学基础之上。
完成以上证明的时项目快照包括:
- 超过 99.4万行Lean代码 ;
- 超过 850个代码文件 ;
- 系统共查阅 15部书籍与论文、共1037页 ,其中约三分之二是在证明推进过程中逐步发现的。
当然,代码行数只能展现工程体量的一个侧面。如果以Bender–Suzuki定理为终点向前追溯,项目已经形成一个包含30298个数学声明、186187条依赖关系的证明网络,最长依赖链达到458层。如果把Lean基础库中的相关内容也计算在内,这张网络会扩大到74922个声明和超过144万条依赖关系。可以说,近百万行代码背后是一张盘根错节、紧密链接的证明网络。这项研究表明,AI智能体已经可以在机器核验和分层审查的合力作用下,持续推进大型、超长程的数学工程。
项目的实际运行过程同样具有超长程的特征。论文所记录的最长一次智能体执行长达9.17天,期间系统对累积信息进行了606次压缩整理,同时始终保留当前证明目标、已经完成的结果、以及仍待解决的问题。这些数据表明,项目管理着一张不断演化的超长程的证明网络,单次生成或一次对话根本无法覆盖如此复杂的过程。
以往,大规模数学形式化只能高度依赖人工投入,通常需要多位研究者持续协作数年之久。一个可供对比的历史参照:Feit–Thompson定理此前的Rocq形式化版本,由大约15人耗时六年才完成。而FormaTheoria则在七个月内就完成了该人工项目的全部内容,并进一步拓展至其他关键定理的形式化工作。七个月对于一次AI智能体任务而言,仍然是极为漫长的运行周期,但与传统的人工形式化相比,AI的介入显著缩短了项目运行的时间尺度。
△
形式化让文献中隐藏的问题逐一浮出水面
数学文献通常面向熟悉该领域的研究者。因此,作者往往会省略前文已经出现过的条件,或者默认读者能够识别不同定义之间的等价关系。一些细小的排版错误或符号错误,人工阅读时也常常被自然而然的忽略或者纠正。但FormaTheoria做法不同,它将文献逐条翻译成Lean代码时,每一个定义、每一个条件和每一步推理都必须写的清清楚楚、毫不含糊。正是这种逐行核验的严格要求,让原始文献中本来隐而不见的问题变得一目了然。
论文详细记录了项目发现的多种文献问题,包括不同资料对同一概念给出了不一致的定义、定理陈述遗漏了必要条件、整除条件位置写错,甚至证明中的下标也存在误差。其中一部分问题,可以根据文献上下文自动修正;证据不足的问题则会交由数学家进一步判断。
一个典型案例来自两部关于奇数阶定理的资料。两部资料都定义了“类型I极大子群”,但区别在于:其中一部要求某个性质对“每一个补结构”成立;另一部则只要求“存在一个补结构”满足该性质。在形式上,前者显然比后者更强,因而两套定义无法直接对接。FormaTheoria在形式化过程中敏锐地识别出这一差异,随后借助Schur–Zassenhaus定理,证明两种定义在这里实际等价,从而成功搭建起连接两部文献的桥梁。
另一个案例来自Peterfalvi的一条引理。该引理的正式陈述中遗漏了“某个群的阶为奇数”这一前提条件,然而后续证明实际离不开这个条件。尽管在后文应用该引理时,前文已经保证了这一条件,整体论证并未中断,但Lean不会自动补上这一层背景信息。FormaTheoria在追踪该引理的证明路径和使用位置之后,自动将遗漏的条件明确加入了定理陈述,使整个形式化链条更加完整和可靠。
△
项目还发现了更直接的文献错误。一处定义把本应出现的对象H写成了M,而且两部参考资料保留了相同的错误。Huppert的一条定理则把因子d放进了错误的整除条件中;系统找到反例后终止证明,并将问题交给数学家核查。人工确认了正确的条件。Higman的一段证明还把一组基向量的编号写成了从u0到um,正确范围应当到um−1;这一处下标错误由系统在证明过程中自动识别并修正。
这些案例折射了机器核验对大型数学工程的另一层重要价值。FormaTheoria在构造形式化证明的同时,也对原始文献进行细粒度审查:它记录问题出现在哪里、后续证明需要什么条件、修改依据来自哪些文献,以及修正是否会影响其他结果。对于由数百份资料彼此勾连而构成的CFSG,这种可追踪的审查有机制,能够把那些过去依赖读者经验补全的细节,转化为可以明确检查的数学依据。
未来展望
FormaTheoria目前尚未完成有限单群分类的整体形式化,距离最终目标仍有很长的路要走。项目正在加速推进,持续迈向完整形式化这一现代数学中规模最为庞大的证明工程之一。现有结果表明,AI已经能够在数月内维护并扩展大规模数学环境,跨越多部文献追踪复杂的依赖关系,在严格核验下构建彼此连通、体量客观的理论体系。AI的能力边界,也由此开始从求解孤立的数学问题,逐步拓展至参与系统性的数学知识建构。
这项工作还将形成一套可持续扩展、可重复使用的数学基础设施。传统文献只能告诉读者“证明写在哪里”;形式化代码进一步记录“每个结论依赖什么”“不同来源如何衔接”“哪些问题经过修正”,并将已经核验的定义、引理和证明整理成为可供后续研究直接调用的知识模块。未来一旦加入解释、搜索和可视化工具后,这套知识网络有望帮助研究者更快地理解CFSG的整体结构、复用已有成果,甚至为人类数学家探索新的联系和发现新的定理提供有力支撑。
FormaTheoria项目组希望探索一种面向AI时代的人机协作模式:人类负责确定值得研究的问题并作出关键判断,AI承担大规模搜索与推导,形式系统则确保每一个被接受的步骤都可以被重新检验。当一项证明庞大到任何个人都难以从头复核时,这三者结合的方式,或许将成为人类管理超大规模数学知识的一条全新路径。
说明:文中的项目状态和定量结果来自论文所述的2026年8月完成时的快照。
论文:https://arxiv.org/abs/2608.10894
代码:https://github.com/Qiuzhen-CFSG/CFSG
本文来自微信公众号“量子位”,作者:FormaTheoria 团队
