中国科学家首次以书生科学多模态大模型攻克世界级数学难题

困扰数学界 30 余年的三维 Ghys 猜想被破解。上海人工智能实验室（上海 AI 实验室）访问学者、大湾区大学教授许地生团队，依托书生科学多模态大模型 S2（书生 -S2），基于 " 通专融合 " 技术路径，通过人机协同完成了三维 Ghys 猜想的证明。北京大学董彬教授、刘若川院士团队用其开发的 SHEAF 框架做了形式化验证，确认其正确性。这是中国科学家第一次用中国大模型攻克世界级数学难题。

Ghys 猜想由法国数学家艾蒂安 · 吉斯（ tienne Ghys）在 1995 年提出：每一个紧致复流形上的全纯 Anosov 系统，都双全纯共轭于某个复 infra- 幂零流形上的全纯仿射自同构，被动力系统领域专家公认为最重要的长期公开问题之一。相关论文已在 arXiv 发布，形式化代码也在 GitHub 公开。

Ghys 猜想：为混沌系统寻找 " 底层代码 "

Ghys 猜想的核心是：混沌的动力系统行为的存在，能否决定几何上的分类。如果成立，混乱的动力学轨迹问题就能化归为简洁规整的标准代数模型。

可以想象一个封闭有限、没有边界、每一小块都遵守复数运算规则的 " 世界 "。对 Anosov 系统，可借揉面作类比——按压、延展、折叠面团，一些方向被拉伸、一些被压缩；拉伸让初始紧邻的点快速分离，初始条件的微小差异会带来截然不同的演化结果。Ghys 猜想是说：只要存在这样一种 " 既像揉面又完全规则 " 的运动，这个 " 世界 " 就只能长成一种由简单规则反复拼接、像晶体格子般高度规整的形状，比如复环面；反过来看，这个运动本质上只是这个 " 世界 " 的简单平移、旋转或缩放。运动方式越混沌，反而越限制世界只能长成什么形状。

2026 年国际数学家大会 45 分钟报告人、北京大学北京国际数学研究中心谢俊逸教授评价："Ghys 猜想的难点在于其对应的实数版本的类似断言仍是著名的完全公开的难题，复数的情形问题变得更加刚性，是复动力系统刚性现象研究中的重要问题，非常困难。"

许地生长期深耕这一猜想，曾与导师、菲尔兹奖得主阿图尔 · 阿维拉（Avila）合作研究三维情形，但未形成有效证明思路；此后他与学生张洁松合作取得部分弱相关结果，刊发于数学顶级期刊《欧洲数学会杂志》（JEMS）。

7 批接续推演、389 个节点：人机协同的关键突破

上海人工智能实验室主任、首席科学家周伯文有一个判断：问题越古老、越基础，AI 提效的空间越大，三维 Ghys 猜想正是这类基础难题中的一个。

2026 年 3 月，许地生成为上海 AI 实验室访问学者，双方组建联合团队，并搭建了面向数学研究场景的 Harness 系统。许地生精准指出模型与系统的能力短板，依托真实前沿数学命题驱动系统多轮迭代打磨。8 月，内部迭代成型的书生 -S2 及配套系统具备大规模递归推理能力与高灵活的人机交互能力，在复杂数学命题处理上实现质的跃升。针对三维 Ghys 猜想的首轮推理，书生 -S2 就产出了 400 页推导报告。

训练策略上，团队坚持 " 通专融合 " 路线：在大规模科学知识预训练夯实底座的基础上，构造研究级后训练数据，包括来自数学论文的大规模难题和可靠的校验方案。训练算法上，团队突破了异步长程推理强化学习训练方法，在可验证奖励下破解了误差指数级累积、长期状态维护、自我纠错等难题；还研发了把 Harness 能力提升反向蒸馏回模型的自进化算法，在超出模型直推能力边界的高难度问题上持续获得有效监督信号。在 IMO-Proof、AdvancedMathBench 等强调长程严谨推理的基准上，书生 -S2 整体领先现有开源模型，部分指标超越 Gemini 3.1 Pro 等顶尖闭源模型。

但距离真正破解世界级难题还差一步，关键在更紧密的人机协同：书生 -S2 发挥长链条大规模推演优势，铺开多条支线同步尝试、拆解复杂命题、猜想不同思路，承接海量繁琐推导；研究人员则把握大方向，判断哪些思路值得深挖、哪些是死胡同，给出直觉建议，作为系统下一轮迭代的指令。二者在多轮对话与反馈中紧密互动、迭代推进，而非单方独立推导。

在 AI 首轮探索基础上，许地生与张洁松敏锐抓住关键突破口，持续给模型反馈、校准探索方向。攻关中，书生 -S2 先后完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出上千页严密推导，同时生成数十种全新论证思路，最终助力团队破解这一难题，得到该方向国际前沿学者 " 思考深度远超预期 " 的评价。有意思的是，论文上传 arXiv 之前，动力系统专家谢俊逸也曾用 GPT-6 挑战这道题，并未找到证明方案。这既印证了书生 -S2 的独特价值，也说明中国的大模型同样有能力站上前沿数学的赛场。

北大团队给出专业形式化验证

AI 助力产出的成果是否经得起验证？北京大学董彬教授、刘若川院士团队完成了本次论文全部四个主定理的形式化验证，证明已通过 Lean 检验。团队骨干成员姜杰东、吴彬介绍，整个过程仅约 5 天，峰值并发达 100 个智能体，产出约 55 万行 Lean 代码，专家确认形式化陈述与论文主定理语义一致。

形式化的难度首先来自数学本身：自然语言证明常依赖读者的数学知识补全条件与推理，形式化则须把它落实为计算机可检查的完整证明；论文引用的结果若未进入基础定理库，还需补充形式化证明或另寻替代路线。动力系统领域原有形式化基础设施不足，此次补充了大量基础设施。大量智能体并行时，还须确保各部分的定义、陈述和依赖相互衔接，局部证明才能组成完整证明链。

为组织这一过程，北大团队使用了自主开发的 SHEAF 框架：多个智能体把论文中的命题、定义及依赖关系，组织成一张从目标定理逐层延伸到基础定理库的有向无环图；模型在框架下参与命题分解与形式化证明构建，团队围绕该图编排工作，跟踪各节点的陈述、证明与剪枝状态，把大规模任务分解为相互衔接、可检查的步骤。

早在 2021 年大模型尚未问世之时，北京大学北京国际数学研究中心董彬教授团队便敏锐洞察到人工智能将重塑数学研究范式。北大数学团队是国际上最早布局 AI for Math 方向的研究团队之一，搭建起覆盖高难度评测集（FATE）、大规模数学知识检索（Matlas/LeanSearch）、自动推理与形式化验证（Rethlas/Archon/Danus/Iteris）的完整技术链条；其开发的 AI 系统成功攻克安德森猜想这一公开数学难题，实现国内首例、同时也是国际上首个由高校团队主导，依托人工智能自主突破重大数学猜想的成果。近期，团队还独立完成了庞加莱猜想的形式化验证工作。

本项研究还验证了一种新的科研范式：传统数学研究依赖个体天才的漫长摸索，本次攻关把专家直觉系统性接入机器求解回路，形成 " 系统探索—专家判断—成果积累—反馈修正 " 的闭环。这一范式可复制推广到更多 " 搜索空间巨大而专家稀缺 " 的基础研究领域，实现更多 " 从 0 到 1" 的原始创新突破。（本文首发于钛媒体 APP，作者｜李婧滢，编辑｜刘洋雪）