中国科学家首次用国产大模型攻克世界级数学难题：书生-S2破解三维Ghys猜想

2026年10月15日，上海人工智能实验室（上海AI实验室）宣布，困扰数学界30余年的世界级难题——三维Ghys猜想被成功破解。该实验室访问学者、大湾区大学教授许地生团队依托“书生”科学多模态大模型S2（书生-S2），基于“通专融合”技术路径，通过人机协同完成了证明。北京大学董彬教授、刘若川院士团队利用自主研发的SHEAF框架对证明完成形式化验证，确认其正确性。

相关论文以《Codimension-one holomorphic Anosov diffeomorphisms》为题发表于预印本平台arXiv，形式化代码已在GitHub公开。论文作者为就职于瑞典皇家理工学院（KTH）的张洁松博士，他在致谢中特别感谢许地生促成其以访问学者身份在上海AI实验室访学，并提到“论文的主要思想正是在访学期间成形”。

千页推导与五天验证

这场攻关始于一次数学竞赛。2025年，中国数学会中学数学竞赛委员会在全国中学生数学奥林匹克（CMO）首设AI测试，书生系列的前代模型书生-S1取得102分，在参评大模型中排名第一，远超78分的金牌线，其答卷被阅卷专家评价为“答案表达方式非常接近人类”。长期深耕动力系统领域的许地生教授由此关注到书生大模型的数学潜力，2026年3月成为上海AI实验室访问学者，双方组建联合团队并搭建面向数学研究场景的Harness系统。

从2026年8月起，书生-S2从多个角度对猜想展开试探。针对猜想的首轮推理，模型就产出了400页推导报告；整个攻关过程中，书生-S2先后完成7批接续推演，问题图从15个节点扩展到389个节点，输出总量达千页量级，同时生成数十种全新论证思路。模型承担海量繁琐的长链条推演，数学家则负责把握方向、甄别死胡同、给出直觉建议，双方多轮反馈迭代，最终拼出完整证明链。

证明的可靠性由第三方独立把关。北大团队基于SHEAF框架组织大规模智能体并行工作，仅用时约5天、峰值并发约100个智能体，产出约55万行Lean代码，完成全部主定理的形式化验证。据上海AI实验室官方稿件介绍，专家确认形式化陈述与论文主定理语义一致，Lean检验确保了证明的严格正确性。

三维Ghys猜想

这个猜想由法国数学家Étienne Ghys于1995年提出，被公认为动力系统领域最重要的公开难题之一。

可以用一张“猫脸”图（阿诺德猫映射）来理解这个猜想：把一张猫的照片当作一个正方形世界，按照公式T(x,y)=(2x+y, x+y)反复变换——每变一次，猫就被拉伸、剪切、撕裂一次，散落的碎片再折回正方形内。迭代两三次后，猫脸已经面目全非；到第7次、第11次时，肉眼看只剩一片均匀的灰色。但混乱只是表象：猫脸被撕得越碎，其实越说明这个系统在不断拉伸、压缩——这正是数学里“混沌”的标准样子，也是Ghys猜想研究的对象（Anosov系统）：看似一片混乱，实则每一步都严格服从确定的规则。

Ghys猜想问的是：如果一个几何世界（比如一个封闭的曲面或空间）里存在这种“一边混乱、一边守规则”的运动，那么这个世界本身会是什么形状？答案出人意料：只能是极度规整的形状，比如像晶体格子一样、由简单规则重复拼接出来的“复环面”。也就是说，表面上的混乱，反而把这个世界可能的几何形状彻底锁死了。猜想的意义在于：一旦确认混乱存在，复杂轨迹的问题就能被化简成标准的代数模型，等于找到了混沌系统的“底层代码”。

书生-S2是什么？

书生-S2是书生系列科学多模态大模型的最新一代。公开信息显示，书生-S2（Intern-S2-397B）为3970亿参数规模的开源模型，于2026年9月在上海浦江创新论坛发布，以Apache-2.0协议开源；其核心创新“Memory Decoder”（记忆解码器）可将蛋白质序列、化学分子式等领域知识训练成可插拔的外部记忆模块，接入时无需改动主模型参数，从而低成本拓展专业能力。

在上海AI实验室的规划中，书生-S2还将作为智能中枢接入“书生·端砚”科学发现平台——该平台已于2026年7月在WAIC科学前沿论坛发布，面向生命科学、关键材料、半导体、核聚变、量子、地球气象六大科研领域落地。

其研发方上海人工智能实验室是我国人工智能领域的新型科研机构，并非一家商业公司。自2023年书生大模型首次发布以来，实验室已构建起书生大模型家族：大语言模型书生·浦语（InternLM）、多模态模型书生·万象（InternVL）、科学多模态模型Intern-S1系列与强推理模型书生·思客（InternThinker），并配套开源了训练框架XTuner、推理框架LMDeploy、评测框架OpenCompass等全链路工具。其中Intern-S1于2025年7月发布，官方称其在关键科学任务上的性能超越Grok 4。

本次攻关中，书生-S2在IMO-Proof、AdvancedMathBench等强调长程严谨推理的基准上整体领先现有开源模型，据上海AI实验室官方稿件，其在部分指标上超越Gemini 3.1 Pro等顶尖闭源模型。

还有哪些“数学专用”模型？

在使用AI模型破解数学难题方面，全球主要科技公司已基本全部入局，形成了两条技术路线：一条是“通用推理模型做数学”，另一条是“专用证明模型+形式化验证”。

在“通用推理”路线上，布局最深的是谷歌DeepMind。其旗下既有面向奥赛的AlphaGeometry系列几何证明器——AlphaGeometry 2已能解出84%的IMO几何题（42/50），达到金牌选手水平——也有靠强化学习在Lean形式语言中搜索证明的AlphaProof，以及其升级版研究智能体AlphaProof Nexus。

（AlphaGeometry接近奥赛金牌选手水平）

2026年2月，DeepMind还发布了以Gemini Deep Think为底座的数学研究智能体Aletheia，无需人工干预即从700个厄尔多斯猜想中自主解决了4个开放问题。

OpenAI走的是另一条路：其未公开的通用推理模型并未经过专门的数学训练，却在2026年5月推翻了厄尔多斯单位距离猜想，并在同年10月一次性公开722篇AI生成的数学手稿。美国初创公司Harmonic的Aristotle则以“机器可验证”为卖点，用Lean直接输出证明。

在“专用证明模型”路线上，中国公司阵容齐整。深度求索（DeepSeek）的DeepSeekMath-V2在IMO-ProofBench高级子任务上得分61.9，超过GPT-5.2-Thinking；其DeepSeek-Prover-V2是Lean 4形式化证明领域的开源标杆。

月之暗面（Moonshot AI）与Numina合作开源的Kimina-Prover、字节跳动的Seed-Prover系列，同普林斯顿大学研发的Goedel-Prover-V2一道，构成Lean证明模型的开源主力。竞赛数学方面，小红书自研的dots-note-3.0在2026年IMO上拿下42/42的史上首个满分。

此次三维Ghys猜想的突破，首次证明了国产大模型不仅能拿竞赛金牌，还能在数学家主导的人机协同模式下，产出经机器严格验证的世界级研究成果。正如上海AI实验室主任周伯文的判断——问题越古老、越基础，AI提效的空间越大。接下来，团队计划将这次跑通的能力闭环封装进“书生·端砚”平台，向更多“搜索空间巨大而专家稀缺”的基础研究领域复制。