7个月完成多项关键定理形式化：AI助力CFSG验证，加速超大规模数学证明工程

FormaTheoria七个月完成多项关键定理形式化AI助力CFSG验证加速有限单群分类CFSG在现代数学中是规模最为庞大的证明工程之一。这项证明由上百位数学家耗时数十年接力完成成果散落在数百篇论文与专著中总篇幅接近两万页远超单人或单个团队完整复核的能力。在此背景下引入AI辅助进行大规模形式化验证成为新方向。在丘成桐先生倡导下来自清华大学求真书院领军班学生以及丘成桐数学科学中心、智能产业研究院和华威大学的研究团队提出了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猜想等。GFSG的应用价值获国际数学界最高层级认可。2014年国际数学家大会邀请2018年美国数学会Cole代数学奖得主Robert Guralnick作相关专题报告。这些应用包含重要学术成果CFSG是限制Burnside问题完整证明链的关键环节Efim Zelmanov因解决该问题获1994年菲尔兹奖。Smith专著还将有限单群上的Waring问题和扩展图等列为重要应用方向相关代表性论文发表于《Annals of Mathematics》。这表明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的引理陈述遗漏“某个群的阶为奇数”前提后续证明依赖该条件。FormaTheoria追踪证明路径和使用位置将遗漏条件加入定理陈述使形式化链条更完整可靠。此外项目还发现文献错误。一处定义将对象H写成M两部参考资料都有此错误Huppert的定理将因子d放入错误整除条件系统找到反例后交数学家核查确认正确条件Higman的证明基向量编号范围错误系统自动识别并修正。这些案例体现机器核验对大型数学工程的重要价值。FormaTheoria构造形式化证明时对原始文献细粒度审查记录问题位置、所需条件、修改依据及对其他结果的影响。对CFSG而言这种可追踪审查机制能将依赖读者经验补全的细节转化为可检查的数学依据。未来展望FormaTheoria尚未完成有限单群分类整体形式化距最终目标尚远但项目正在加速推进。现有结果表明AI能在数月内维护和扩展大规模数学环境追踪复杂依赖关系构建连通、有规模的理论体系。AI能力从求解孤立问题拓展到参与系统性数学知识建构。该工作将形成可持续扩展、可重复使用的数学基础设施。传统文献只告知“证明位置”形式化代码记录“结论依赖”“来源衔接”“问题修正”并整理核验内容为知识模块。加入解释、搜索和可视化工具后知识网络有望助研究者理解CFSG结构、复用成果为数学家探索新联系、发现新定理提供支撑。FormaTheoria项目组希望探索AI时代人机协作模式人类确定研究问题并做关键判断AI承担大规模搜索与推导形式系统确保步骤可重新检验。当证明庞大到个人难以复核时三者结合或许是管理超大规模数学知识的新路径。说明文中项目状态和定量结果来自论文所述2026年8月完成时的快照。