当顶尖数学家遇到AI科学家，一道65年的拓扑难题被逐行核验。
2026年秋以来，AI参与前沿数学研究与验证的进展接踵而至。9月，Anthropic和OpenAI先后报告，完成了费马大定理和带光滑外力的三维Navier–Stokes方程爆破的Lean形式化证明。10月，OpenAI一次性发布722篇数学结果手稿，部分伴有Lean形式化证明。
这些成果背后，是长期积累的数学知识。一篇论文的证明，往往依赖大量参考文献中的定义、定理和方法。而数学研究中，还有一类成果将理论论证与大规模计算紧密结合，程序、计算数据和论文推导共同构成对数学命题的完整论证。126维Kervaire问题的证明就是一个例子：这一延续65年的拓扑难题，其最后一步的证明除了依赖大量前期文献，还依赖数百万条计算记录。
怎样确认纸面上的论证、程序中的计算，以及最终得到的结论，真正连接在一起？
进一步说，当这些论证和计算能够接受可靠核查，我们又该怎样理解它们，并把其中有用的思想和工具带入未来的研究？
得益于上海创智学院“研创学”一体化机制与开放、多学科交叉的平台环境，上海创智学院刘鹏飞研究团队与复旦大学上海数学中心首席教授王国祯团队共同组建Kervaire 126项目联合攻关小组，正在围绕这两个问题展开实践。
今天，Kervaire 126项目团队宣布，借助AI完成了126维Kervaire问题主论证的Lean形式化，并建立了支撑证明的大规模计算认证框架。团队在核查证明过程中积累的形式化理论与计算认证工具，也为AI参与这一领域的后续探索提供了基础。团队同步公开了项目主页，并开源了主论证的Lean形式化代码，供研究者了解工作进展、查阅证明细节，并在此基础上开展进一步研究。
● 项目主页：https://gair-nlp.github.io/Kervaire126/
● 项目仓库：https://github.com/GAIR-NLP/Kervaire126
Kervaire 126项目主仓库形式化内容分布（截至2026年10月31日）。
一、形式化如何辅助数学成果的验证？
一项数学成果，通常由以下三部分组成：数学内涵、数学论述和辅助材料。
● 数学内涵：研究者真正希望研究的对象、条件和结论，涵盖希望理解的结构、建立的联系与解决的问题。
● 数学论述：通过定义、命题和论证表达数学内涵，通常以论文的形式呈现。
● 辅助材料：支撑论述的数据、程序、计算结果与图表。它们记录计算过程、提供推理依据，与论文中的数学论述共同支撑结论。
数学论述需要引导读者理解证明。作者通常着重展开新颖、困难的部分，让读者在关键思路处慢下来；对于依照已有方法即可完成的常规检查，则往往略去琐碎细节，留给读者结合背景知识补全。
这样的取舍有助于突出证明的核心，也意味着纸面上的论证并不逐项列出所有检查。论文里一句“由前面的定理可得”，熟悉这个领域的读者也许就能接着往下读。但这句话里藏着一个具体问题：那个定理要求的条件，在这里都满足吗？在Kervaire 126的证明中，这样的问题随着计算结果的引入，变得更为复杂——核查这些论证，需要将计算表里的260多万条记录与此前得到的结论逐一对照。
（一）论文略去的步骤，Lean怎样核查？
形式化证明工具Lean为这些细节的严格核查提供了方法。研究者将数学定义、命题及其证明转写为Lean能够检查的形式，明确每一步推导的依据，并补齐论文中省略的步骤。这一过程称为证明的形式化。Lean按照严格的逻辑规则，检查定理的适用条件是否满足、结论能否从给定的前提推出。这样，繁多的推导细节可以接受机器逐项核查，读者则能够将更多注意力放在证明的关键思想上。
与此同时，推导通过检查，并不自动意味着形式化表达准确体现了原有的数学内涵。论文中默认的约定是否得到完整表达，程序数据是否对应所研究的数学对象，形式化命题的条件与结论是否忠实于原论文，仍需要数学专家进行对齐检查。
形式化可以用于不同来源的证明：既包括数学家给出的理论证明，也包括程序或大模型参与产生的证明。下图按原始证明的产生方式整理了一些代表性成果，并展示其形式化覆盖程度。
二、Kervaire 126是什么？
对空间进行分类，是拓扑学的基本问题。同一个拓扑空间可能具有不同的光滑结构：20世纪50年代，John Milnor发现，在所有七维空间中，存在与通常球面拓扑相同、光滑结构却不同的“异构球面”。理解这些差异，是高维几何研究的重要课题，Kervaire不变量问题与此密切相关。
Kervaire不变量取值为0或1，用于刻画带有特定附加结构的流形的一种几何障碍。哪些维数中存在这一不变量为1的标架流形，是一个延续六十多年的问题。2024年，林伟南、王国祯和徐宙利在《On the Last Kervaire Invariant Problem》中宣称解决了最后一个悬而未决的情形：126维。结合此前结果，存在维数最终确定为2、6、14、30、62和126。
这一证明研究了球面稳定同伦群中的特定元素，再利用Browder的工作，将相关代数结论转化为几何上的存在性结论。理解和计算稳定同伦群，是拓扑学中最基础、最困难的问题之一。原论文借助Adams谱序列这一分层计算工具，将理论推导与大规模程序计算结合起来，获得证明所需的稳定同伦信息。
本图以球谱S⁰的Adams谱序列E₂页（局部）为底图。数学理论提供推导规则及其适用条件，专用程序据此计算和传播关系。证明图中坐标为（126, 2）的元素h₆²存活到E∞，是解决126维Kervaire问题的关键。
三、Kervaire 126项目做了什么？
Kervaire 126项目围绕原论文的形式化核查展开：一方面检验论文中的理论论证，另一方面认证支撑证明的程序计算，并探索数学家与AI如何分工协作。
对一项数学成果进行完整的形式化，不仅需要形式化论文本身的内容，还需要对论文依赖的所有理论知识和前置结论进行形式化，这可能涉及数十篇重要文献及相关领域背景；特别地，Kervaire 126还依赖于大量程序推导的结果，仅仅是由专用计算程序输出的微分和延拓结论，就有超过267万条。
综合考虑算力资源与后续研究需求，团队分阶段推进形式化工作，目前完成了对论文数学论述的形式化，补全了必要的谱序列基础背景，并建立起足以支持后续研究的配套数学框架；程序结论的认证则作为独立任务并行推进。
（一）数学论述的形式化
项目团队对于《On the Last Kervaire Invariant Problem》论文中的论证进行了形式化验证，在两周时间内，将原论文的证明主线组织为Lean中相互衔接的定义、命题与证明，并搭建配套的数学框架，共生成29万行Lean代码。这使论文中的推导能够逐步接受机器核查，也让不同部分的证明可以在同一环境中调用和组合。在团队的实践中，已形式化的推导细节由内核检查，数学家则持续审阅关键陈述，以及论文、程序数据和Lean对象之间的对应关系。
目前，团队已形式化论文使用的多种关键推导方法，并在明确列出的基础前提与计算输入下，完成主论证及其几何推论的Lean证明。这些成果既用于核查原论文，也为计算认证和进一步探索提供了可复用的工具。
（二）程序计算的验证
原论文使用了《Machine Proofs for Adams Differentials and Extension Problems among CW Spectra》中的专用程序，计算Adams谱序列的基础数据及微分、延拓关系，为部分论证提供计算结果。程序在输出计算结果的同时，也留下了推导日志，记录了程序采用的推导、尝试的可能性及其排除过程。
专用计算程序的输出日志超过267万行，仍省略了一些推理依据。要将这些计算结论全部送入Lean核验，需要补齐日志当中省略的依据、理清结论之间的依赖、区分已经推出的结论与尚在试探的假设，并在Lean中对推理过程进行编译验证，这是一项巨大的工程挑战。
团队采用的验证方案，是从计算结果和推导日志中提取记录、补齐依据，批量生成供Lean核验的“证书”。这些证书说明一次推导使用了哪些输入、依据哪些规则，以及需要核对哪些关系，使大量计算能够按照统一的方法接受检查。与此同时，团队在Lean中证明推理规则与证书检查的可靠性：在所需前提成立时，只要证书通过检查，相应的数学结论就成立。通用的规则和可靠性定理可以反复使用，具体计算则提供各自的证书，共同完成程序数据的验证。
目前，团队已在明确的输入前提下，核验了部分真实日志中的具体推导。完整日志的核验、输入依据的认证及数学对象的对应核查仍在推进。团队也在探索将已验证的推论用于后续计算，减少重复搜索、精简日志，让验证中积累的数学认识继续服务于计算与研究。
（三）碳基与硅基的协作
并行的AI Agent可以在很短的时间内把多个引理写进Lean，尝试构造证明。形式化推进得这样快，团队怎样把握整篇证明的进度？哪些关键步骤已经通过Lean检查，哪些结论还依赖尚待验证的前提，又有哪些地方需要数学家先作判断，AI才能继续？
王国祯教授和学生负责人张家硕在上海创智学院就Kervaire 126的形式化设计展开讨论。
数学家负责确定研究目标并作出数学判断。他们梳理论文的证明思路，明确关键对象、条件与结论，审阅形式化陈述是否表达了原有数学内涵，并在证明遇到困难时判断应如何拆分问题、补充论证或调整方向。
交叉研究者负责面向数学目标组织形式化工程。他们规划研究路线、选择工具、整合资源，将数学思路整理为模块、接口和具体任务，调度AI智能体并把控进度与质量。他们还建设人与AI共同使用的交互系统，减少成员之间及人机之间的协作阻力，追求工程结构的清晰、简洁与接口的可复用性；当接口不足或任务偏离目标时，再与数学家共同调整。
AI负责围绕明确任务推进证明与代码工作。它在已有形式化环境中组合和复用结果，尝试完成证明、补充所需引理，并根据Lean的检查反馈反复修改。遇到缺失条件或接口时，AI提出问题与补充建议，交由人审阅后再继续推进。
协作工具将任务、讨论与审阅连接起来。团队通过GitHub管理代码与审阅，将AI接入即时通信软件，让成员在日常讨论中分配任务、反馈问题和跟进进展。项目看板把论文中的关键命题与对应的Lean声明逐一关联，并标出证明状态和依赖关系。团队可以从主结论往回看，找到仍待证明的引理或需要审阅的前提，再据此安排AI的下一轮任务。
10月，依托前期积累的代码与数学成果，团队组织AI智能体开展大规模并行协作，在大约2周的时间内，完成了论文主论证的形式化。
Kervaire 126项目主仓库形式化内容的演进（2026年10月14—31日）。
四、形式化是终点吗？
当一份证明通过机器检查之后，数学工作还会怎样继续？证明中的关键思想如何被理解，其中的方法如何用于其他问题，又如何带来新的发现？
陶哲轩在《Mathematics in the age of AI》中指出，数学问题的求解还包含正确性核查、思想的解释与传播、共同体的消化与接受，以及融入理论等环节。受这一思路启发，团队结合项目实践，以数学问题的求解为例，提出L1到L5的五阶段框架，描述一项成果从问题提出，到得到核查、理解和应用，再到展现更广泛数学价值的过程。
● L1问题提出 一项数学成果从一个明确的问题出发。问题的表述指明了研究对象、已知条件和需要回答的问题。
● L2解答形成 成果已给出候选证明或反例，支撑这一解答的论证可以逐步核查。
● L3正确性确认 候选解答经过核查，已有充分依据确认其成立。对于通过形式化验证的证明，还需确保语义对齐。
● L4理解与应用 成果的关键思路得到理解。它的结论可以支撑新的证明，它的方法可以用于另一类问题，也可以启发新的解法。
● L5更广泛的数学价值 一项成果可能解释长期未明的现象，揭示看似无关的问题背后的共同结构，或使一个重要的新问题第一次得到清楚的表述。
形式化被视作数学证明正确性的终点。但与此同时，它也将要并正在成为人类和AI理解证明，并进一步开展工作的起点。一方面，形式化大大降低了人与人、人与AI之间的信任成本，帮助人将注意力集中到真正新颖和重要的数学思想中，而不必纠结于繁琐的细节，加速了人类对于新的数学知识的理解。
另一方面，搭建好的形式化环境也为AI发现规律、提出猜想、尝试证明、验证猜想提供了难能可贵的闭环环境。Kervaire 126团队分享了一个实践中的例子：在分析ss程序生成的573条Syn计算记录时，AI从多条记录中识别出相似的推导结构，并据此提炼出结论成立的充分条件。随后，AI以原论文中两个已完成形式化的关键数学工具为基础，在Lean中证明了这条新推论。如果将这条推论规则编写进原来的专用验证程序，573条计算记录的400条都将可以直接推出。
接下来，团队希望通过这种方法，不断扩充专用计算程序中的可靠性规则，得到更高效、简洁的专用计算程序，从而扩展谱序列的可计算范围，拓展人类对于稳定同伦信息的认识边界。
五、研究团队介绍
得益于创智学院多学科交叉的平台环境，团队得以同时汇聚数学领域和AI领域的顶尖人才，让不同领域的认知在这里深度融合。
在数学领域，复旦大学上海数学中心首席教授王国祯曾获陈省身数学奖、陈嘉庚青年科学奖，2026年与菲尔兹奖得主王虹一同获颁求是杰出科学家奖，两人是该年度数学领域仅有的两位获奖者。加州大学洛杉矶分校（UCLA）数学系教授徐宙利是国际知名的代数拓扑学家，曾获2022年K理论奖、受邀在国际数学家大会作报告，并于2023年当选美国数学会会士。上海数学中心青年研究员林伟南专注于稳定同伦理论与计算方法，三人共同完成了攻克126维Kervaire不变量问题的原创性研究。
在AI领域，上海创智学院全时导师刘鹏飞副教授长期从事大模型预训练和数据工程，"提示工程"最早提出者，谷歌学术引用3.4万余次，负责GAIR研究组，探索大模型智能边界与科学知识利用的新方法。
