中国大模型首破世界级数学难题：书生-S2 助力证明三维 Ghys 猜想
一个 1995 年提出的刚性猜想
10 月 15 日，上海人工智能实验室发布消息：困扰数学界三十余年的三维 Ghys（吉斯）猜想迎来破解。上海人工智能实验室访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型 S2（书生-S2），通过人机协同完成了这项证明；北京大学董彬教授、刘若川院士团队利用其开发的 SHEAF 框架完成形式化验证。相关论文已在预印本平台 arXiv 发布，形式化代码在 GitHub 公开。实验室称，这是中国科学家首次用中国大模型攻克世界级数学难题。
猜想说了什么？Ghys 猜想由法国数学家 Étienne Ghys 于 1995 年提出，猜测每一个紧致复流形上的全纯 Anosov 系统，都双全纯共轭于某个复 infra-幂零流形上的全纯仿射自同构。实验室给出的直观是这样：想象一个封闭有限、没有边界、每一小块都遵守复数运算规则的「世界」，如果它上面存在一种「既像揉面又完全规则」的运动，那么这个世界只能是由简单规则反复拼接、像晶体格子一样高度规整的形状，比如复环面；而这个运动本质上只是这个世界里的平移、旋转或缩放。
为什么这件事很难？2026 年国际数学家大会 45 分钟报告人、北京大学谢俊逸教授的评语是：Ghys 猜想的难点在于其对应的实数版本的类似断言，至今仍是著名的完全公开难题，而复数情形变得更加刚性，是复动力系统刚性现象研究中的重要问题，非常困难。许地生曾与导师、菲尔兹奖得主阿图尔·阿维拉合作研究三维情形，但未形成有效的证明思路；此后他与张洁松在三维情形取得部分弱相关结果，相关成果刊发于数学期刊《欧洲数学会杂志》（JEMS）。
起点是一场奥数 AI 测试
突破的起点，是书生大模型在 2025 年全国中学生数学奥林匹克（CMO）决赛中的表现。2025 年，中国数学会中学数学竞赛委员会在 CMO 首次设立 AI 测试，共邀请三家国产大模型参与，与人类选手在相同时长内完成答题，并由官方组织以相同标准阅卷评分。其中书生-S1 取得 102 分，不仅在参评大模型中排名第一，更远超 78 分的金牌线。
阅卷专家对书生-S1 答卷的印象是「答案表达方式非常接近人类」，其中一种解法被描述为巧妙的新解法，在参赛学生的答卷里没有出现过。许地生长期从事动力系统、谱理论、分形几何与 AI4Math 等方向研究，注意到这套模型在数学上的潜力；而拿到 CMO 成绩后的上海人工智能实验室，也在探索把模型能力从竞赛级推向难度更高的研究级数学。双方目标不谋而合，2026 年初正式启动模型训练合作研究。
联合团队同步搭建了面向数学研究场景的 Harness 系统。许地生结合自己的科研经验，指出模型与系统的能力短板，并以真实的前沿数学命题驱动系统完成多轮迭代打磨。迭代成型的书生-S2 及配套系统具备大规模递归推理能力，同时拥有高灵活性的人机交互能力，在复杂数学命题的处理能力上实现了明显跃升。
上千页推导，判断由人来做
攻关过程中，针对三维 Ghys 猜想的首轮推理，书生-S2 就产出了 400 页的推导报告。从 2026 年 8 月起，模型从多个角度对猜想开展试探，前后完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出总量达千页的严密推导，同时生成数十种全新的论证思路，其中不乏新颖构想。
分工是清晰的。模型发挥长链条大规模推演的优势，铺开多条支线同步尝试、拆解复杂命题、把海量繁琐的推导工作承接下来，每一轮迭代给出大量尝试结果；研究人员则负责把握大方向，判断哪些思路值得深挖、哪些路径是死胡同，并给出直觉性的建议，作为系统下一轮迭代的指令。完整的证明链条不是模型独立推出的，而是人与模型多轮对话、彼此启发、一次次试错后拼起来的。论文作者在 arXiv 中声明：使用了 Intern-S2 协助发展数学思想与论证，但由作者独立核验全部数学论证并承担责任。论文由许地生的学生、现就职于瑞典皇家理工学院的张洁松博士完成并整理。论文题为《Codimension-one holomorphic Anosov diffeomorphisms》（余维一的全纯 Anosov 微分同胚），其核心定理证明的是 Ghys 猜想的余维一情形，并特别推出复维数三的情形。
这里需要写准一句话：这次解决的是余维一情形（因而覆盖复三维情形），并不等于整个 Ghys 猜想已被完全解决。论文本身也讨论了高余维情形中存在的障碍，例如某些高维全纯 Anosov 系统的稳定与不稳定分布可能并不全纯，因此一般的高余维版本不能据此宣称已经完成。把「破解三维 Ghys 猜想」与「证明整个 Ghys 猜想」区分开，才是对这项工作最准确的表述。
还有一段有意思的旁证：在论文上传到 arXiv 之前，谢俊逸收到了团队送来的论文。他听说这是由国内模型做出的，特意用 GPT-6 进行了测试，但并未解决该问题。实验室把这件事视为书生-S2 在这次前沿数学探索中独特价值的旁证，也当作一个信号——中国的大模型同样有能力站上前沿数学的赛场。
形式化验证，以及一台「飞轮」
AI 产出的成果能否经得起检验？北京大学董彬、刘若川团队完成了本次论文全部四个主定理的形式化验证，证明已通过 Lean 检验。Lean 是交互式定理证明系统，能对形式化证明进行严格的逻辑检查。北大团队骨干成员姜杰东、吴彬介绍，整个过程仅约 5 天，峰值并发达 100 个智能体，产出约 55 万行 Lean 代码，展现出极大的并行规模与极快的验证速度。专家确认，形式化陈述与论文主定理语义一致。
形式化的难度首先来自数学本身：自然语言的证明常常依赖读者用既有知识补全条件与推理，形式化则必须把这些落实为计算机可以检查的完整证明。论文引用的结果如果没有进入基础定理库，还要补充形式化证明，或寻找利用已有结果的替代路线。动力系统领域原有的形式化基础设施不足，这次工作补充了大量基础设施。为组织这一过程，北大团队使用了自主开发的 SHEAF 框架，把论文中的命题、定义及依赖关系组织成一张从目标定理逐层延伸到基础定理库的有向无环图，再围绕这张图编排工作、跟踪各节点的陈述、证明与剪枝状态。
边界仍要说清楚。Lean 检验的是形式化代码中的逻辑正确性：它能确保所陈述的定理被严格证明，但不能自动保证论文里每一处自然语言表述、建模选择与定理形式化都没有偏差；而 arXiv 上的论文是预印本，也还不等于经过期刊同行评议的正式发表版本。形式化验证与同行评议是两种不同性质的检验，缺一不可。
这项研究的意义不止于一个难题被解决，而在于它验证了一种新的研究范式：传统数学研究依赖个体天才的漫长摸索，而这次攻关把专家直觉系统性地接入了机器求解回路，形成「系统探索—专家判断—成果积累—反馈修正」的闭环。实验室认为，这套范式可以复制推广到更多「搜索空间巨大而专家稀缺」的基础研究领域。接下来，团队打算把这次跑通的完整能力闭环封装为书生·端砚科学发现平台可复用的数学验证模块，供后续科学问题研究直接调用；同时以三维 Ghys 猜想的突破为起点，把沉淀的推理能力扩展应用到数学结构同源的其他学科，取得新突破后再把新能力封装回平台复用，形成「突破—封装—复用—再突破」的自进化飞轮。这套说法能否兑现，要看下一次别的学科问题上的表现。