国产大模型首次加入AI顶级数学天团，攻克31年悬案

► 文 观察者网心智观察所

2026年10月中旬，上海人工智能实验室，一个由人类数学家与国产科学大模型组成的联合团队，成功攻克了悬置31年之久的世界级数学难题：三维吉斯猜想。这个猜想自1995年被提出后，便成了复动力系统领域学者的拦路虎。在arXiv署名发表这篇数学论文的唯一作者张洁松，曾在北京大学师从许地生教授（现任大湾区大学教授），现为瑞典皇家理工学院博士后。这也是中国本土研发的人工智能大模型首次实质性参与并解决世界级纯数学公开猜想。随后，来自北京大学的另一支团队已经用超过550000行的形式化验证代码，为整个证明过程的每一个逻辑步骤打上了绝对可靠的钢印。自此，国产AI大模型正式跨过奥赛做题家的阶段，加入了拓宽知识边界的顶级数学天团。

张洁松

揉面团与复数世界

什么是吉斯猜想？

动力系统研究的是事物随时间演化的规律，比如天体运行、大气流动。在这个领域里，有一类非常迷人的现象叫做结构化混沌。1967年，苏联数学家德米特里·阿诺索夫提出了一种被后人称为阿诺索夫微分同胚的数学模型。我们可以把同胚映射想象成揉面团的过程：把面团在一个方向上用力拉长，同时在另一个方向上把它压扁，然后再折叠起来，过程中不能把面团扯破。在许多情况下，面团表面原本挨得很近的两粒芝麻，经过几次拉伸和挤压后，位置就会变得千差万别，呈现出极其混乱的混沌状态。但是，不管怎么揉，整个面团的宏观形状和体积规律依然保持着某种稳定的结构。

到了1995年，法国里昂高等师范学院的数学家艾蒂安·吉斯发表了一篇探讨全纯阿诺索夫系统的著名论文。他提出了一个极具洞察力的核心问题：如果这个被反复揉捏的面团，存在于一个带有复解析结构的空间里，且揉面团的动作完全尊重这种复数几何的规则（即全纯映射），会发生什么？

实数世界往往像橡皮泥一样有一定的弹性，允许局部的小修小补；而复数世界则具有极强的刚性，牵一发而动全身。吉斯猜想，复数几何的这种高刚性会把狂野的混沌死死锁住。他预言，在紧致复流形上，任何全纯阿诺索夫微分同胚都不得胡闹，它们在全纯等价的意义下，必然等同于一类极其标准、极其简洁的代数模型，也就是复次幂零流形上的仿射自同构。也就是说，复数空间的规矩太大了，留给混沌自由发挥的余地几乎为零，最终的运动形式本质上全都是最基础的线性代数能够描述的标准动作。

吉斯本人在1995年的论文里，顺手就证明了二维复曲面上的情况，那时候大家觉得高维度的情况应该也是顺手推舟得事。可谁也没想到，一旦从二维跨入三维及更高维度，难度暴增，这道题一卡就是31年。症结在于，当复维度达到三或者更高时，一个在拓扑形态上看来跟普通实数圆环面（如同甜甜圈表面）一模一样的紧致复流形，未必就是一个标准的复圆环面。高维空间里会冒出许多非标准的、奇异的复结构，原本在二维空间里百试百灵的数学工具，到了三维空间全部失效。要证明三维吉斯猜想，就必须把这些奇形怪状的非标准结构一一排除，过去31年里，这件事成了无数数学家的噩梦。

直到张洁松将一篇17页的论文提交到预印本平台，并于10月5日进行了修订，彻底解决了余维数为1的情形。所谓余维数为1，指的是映射的两个特征子丛中，至少有一个的复维度为1。在三维复流形上，两个非零特征子丛的维度加起来正好是3，必然有一个维度是1，另一个是2，所以这项成果严丝合缝地彻底囊括了紧致三维复流形上的所有情况，将悬置31年的三维吉斯猜想一举拿下。

7轮接力与389个节点的头脑风暴

这场漂亮仗的起点，其实源于一场中学生数学竞赛。2025年，中国数学会首次在全国中学生数学奥林匹克竞赛中设立了人工智能测试赛道，邀请国内大模型与顶尖人类高中生同场竞技、统一阅卷。上海人工智能实验室的书生大模型初代版本拿下了102分的高分，远超78分的金牌线，高居参评模型榜首。这一战让大湾区大学理学院教授许地生看到了国产大模型在深层数学推理上的惊人潜力。许地生长期深耕复动力系统领域，此前就在三维吉斯猜想上同他的博士生张洁松一起取得过阶段性成果。2026年初，许地生受聘为上海人工智能实验室访问学者，决定与实验室团队联手，把大模型的能力从解答已有标准答案的奥赛题，推向探索未知无人区的科研级难题。随后，张洁松也加入了这个联合攻关组。

为了啃下三维吉斯猜想这块硬骨头，研究团队于2026年8月正式启动了针对该猜想的密集攻关。他们依靠的核心武器，是上海人工智能实验室在2026年9月13日第19届浦江创新论坛上正式发布的科学多模态大模型书生S2，以及实验室专门为大规模数学递归推演和高带宽人机交互量身打造的支撑系统。书生S2在架构上采用了带有可插拔专业知识模块的记忆解码器，无需重新训练基础权重就能直接嵌入前沿数学语料库，并且经过了先进的异步长周期推理强化学习训练。实验室内部评测显示，在需要严密逐步推导的国际数学奥林匹克证明基准以及高等数学基准测试中，书生S2的表现已经可以与谷歌的顶尖闭源模型Gemini 3.1专业版平起平坐。

在实际攻关中，团队采用了通专融合的深度人机协同模式。大模型与人类学者既没有各自为战，也没让人类沦为单纯的旁观者，双方展开了7轮高强度的接力迭代。在每一轮循环中，书生S2就像一个不知疲倦的超级学术侦探，快速梳理海量的相关数学文献，将宏大的主命题拆解成若干个子命题，并在多个证明分支上同步展开并行探索。它会一步步检验逻辑的自洽性，快速测试各种候选方案。在首轮推理中，它一口气就吐出了400页的推导报告。

面对机器生成的数千页初步推导和几十种截然不同的数学路径，许地生和张洁松发挥了人类顶尖数学家的战略直觉。机器探索出的很多分支其实是走不通的死胡同，人类学者在每一轮结束后，都会仔细审阅机器的输出，依靠深厚的领域经验识别出哪些分支真正具有解析潜力，精准指出模型的短板，然后把直觉建议和方向校准作为指令反馈给下一轮推演。大模型承担了海量假设生成和繁琐步骤检验的组合爆炸式重任，人类则牢牢把控着战略航向，防止搜索过程在死胡同里耗尽算力。历经7轮的反复碰撞与打磨，整个证明图谱上的数学命题和子结果节点，从最初的15个一路疯长到了389个。最终，一条穿过重重迷雾的完整证明路径清晰地浮现出来，其解析深度令熟悉该领域的同行都感到惊叹。

550000行代码筑起的数字铁壁

大模型协助人类写出了非形式化的数学证明，问题也随之而来：面对如此复杂且有AI深度参与的前沿推演，怎么敢百分之百确定它是对的？人类审稿人在面对几十页乃至上百页的高深推导时，难免会因为视觉疲劳或思维定式，放过一些极其隐蔽的逻辑跳跃。

这一次，来自北京大学的另一支独立团队给了定心丸。北京大学董彬教授与刘若川院士领衔的团队，利用著名的定理证明器Lean系统（目前广泛使用的是其第4代版本），结合他们自主研发的专门面向复动力系统的层框架，对这篇新出炉的证明展开了地毯式的形式化验证。

Lean定理证明器最早由计算机科学家兼数学家莱昂纳多·德·莫拉在微软研究院工作期间创立，自2023年起由专门的非营利研究组织维护。截至2025年5月，它的数学库里已经积累了超过210000条定理和100000个定义，此前曾成功检验过彼得·舒尔茨的液态张量实验以及陶哲轩的多项式弗赖曼-鲁扎猜想等重大成果。在这个系统里做形式化验证，要求严苛得变态：数学论文里的每一句自然语言推理，都必须翻译成机器可读的严格代码，由底层的软件证明内核逐一核对是否绝对符合基本公理。在这里，绝对不允许出现任何诸如显而易见、同理可得之类的模糊过渡，也不允许靠读者的直觉去填补一丁点逻辑缝隙。一段证明代码要么彻底编译通过，代表逻辑天衣无缝；要么直接报错，没有任何讨价还价的余地。

北大团队调动了多达100个并行运行的人工智能体，昼夜不停，连续奋战了大约5天。最终，他们生成了超过550000行Lean系统代码，将支撑整个结果的4个核心主定理审了个底朝天，确认其逻辑完全自洽。这项庞大的工程还顺带结出了一个泽被后世的副产品：在过去，复动力系统理论在Lean系统里完全是一片空白，没有任何现成的数字化基础设施；而北大团队在这次验证中构建起的层框架，成为了全球首个经过计算机严格验证的复动力系统形式化基础库，未来的学者再研究同类问题时，可以直接站在这个坚实的数字地基上往上盖楼。

更让人安心的是，这550000行验证代码已经在开源代码托管平台上向全球公开。这意味着，地球上任何一个安装了第4代Lean系统的数学家，只要有一台现代工作站和足够的时间，都可以自己动手把代码下载下来跑一遍编译，亲自验证北大团队的结论。这种极致的透明度在科学界难能可贵。

当然，机器验证也并非绝对的免死金牌。它只能保证在选定的公理体系和特定的形式化编码下，推导过程没有漏洞，但无法防范公理本身选错，或是自然语言命题在翻译成代码时出现语义偏差，更无法完全排除软件内核自身的缺陷。就在2026年早些时候，国际上曾有一名研究人员宣称用Lean系统完成了一份针对著名数学难题考拉兹猜想的证伪，引发轩然大波。后来经过深入调查才发现，那个所谓的证明其实是钻了Lean系统软件内核里一个程序漏洞的空子；等开发人员把这个漏洞修补好之后，那份证伪代码瞬间就无法编译通过了。这个插曲也给学界提了个醒，面对550000行这种人类根本不可能逐行肉眼审查的代码体量，系统的可靠性完全系于内核自身的健康度。好在截至目前，三维吉斯猜想的验证代码完全经受住了考验，没有发现任何异常。

狂飙突进的数学天团

放眼2025年至2026年的全球科技版图，AI进军高阶数学早已是一场群雄逐鹿的国际竞赛。而中国书生S2此次在三维吉斯猜想上的亮眼表现，不仅拿出了实打实的31年公开难题突破，更难得地同时集齐了长达数月的详尽人机交互记录与完备的机器形式化验证，正式宣告中国大模型在前沿数学探索的最高舞台上占据了重要一席。上海人工智能实验室也表示，未来计划将这套包含支撑系统、人机迭代循环与形式化验证流水线的方法论，全面打包进书生·端言科学发现平台，去连接生命科学、材料科学和量子计算等领域的实验设备与数据基础设施。

来源|心智观察所

禁止转载