困扰数学界 30 年的三维 Ghys 猜想被攻破：中国大模型书生-S2 用 5 天"想"出证明，Lean 全量机器验证
🧩 困扰数学界 30 年的三维 Ghys 猜想被攻破：中国大模型书生-S2 用 5 天"想"出证明，Lean 全量机器验证
上海AI实验室 × 大湾区大学 × 北大联手：AI 出千页推演，数学家做方向判断
又一数学难题被 AI 攻破，这次的主角是国产大模型。
上海人工智能实验室 10 月 15 日发布消息：困扰数学界 30 余年的世界级难题——三维 Ghys（吉斯）猜想被成功证明。完成这项工作的是上海AI实验室访问学者、大湾区大学教授许地生团队，他们依托上海AI实验室的"书生"科学多模态大模型 S2（书生-S2），通过"人机协同"的方式完成证明；北京大学董彬教授、刘若川院士团队随后用自主研发的框架对证明做了形式化验证，确认无误。
官方称，这标志着中国科学家首次用中国大模型攻克世界级数学难题。
- 什么难题：1995 年由法国数学家 Étienne Ghys 提出，复动力系统领域 30 余年的公开难题，是检验高阶数学推理的试金石
- 谁做的：上海AI实验室访问学者、大湾区大学许地生团队，依托书生-S2 人机协同完成证明
- 可验证：北大董彬、刘若川团队用 SHEAF 框架形式化全部 4 个主定理，通过 Lean 机器检验
- 规模：AI 完成 7 批接续推演、问题图 15→389 节点、千页推导；形式化约 5 天、峰值 100 个智能体、约 55 万行 Lean 代码
🧮 这道题到底难在哪
用一句话说清 Ghys 猜想
它问的是：一个"混沌"的动力系统，它的运动方式能不能反过来决定这个世界的几何形状？
可以想象一个封闭、有限、没有边界、每一小块都遵守复数运算规则的"世界"。在这个世界里，有一种"既像揉面团、又完全规则"的运动（数学上叫 Anosov 系统）：面团被按压、延展、折叠，有些方向被拉伸、有些被压缩，初始时挨得很近的点会迅速分离——这正是"混沌"的来源。
Ghys 猜想说：只要存在这样一种运动，那这个世界就只能长成一种"像晶体格子一样高度规整"的形状（例如复环面），而这种运动本质上只是简单的平移、旋转或缩放。
难点还在"对照系"：Ghys 猜想对应的实（数）版本类似断言，至今仍是全球公开未解难题；复数情形反而变得更加"刚性"，是复动力系统刚性现象研究中的重要问题。正因如此，它被动力系统领域专家公认为该领域最重要的长期公开问题之一。
🤝 谁做的、怎么做的
这不是"AI 独立秒解"，而是人机协同：
| 分工 | 做了什么 |
|---|---|
| AI 侧（书生-S2） | 承担大规模、长链条复杂数学推演：首轮即产出 400 页推导报告；攻关中完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出总量达千页，并生成数十种全新论证思路 |
| 人侧（数学家） | 把握研究方向、判断哪些思路值得深挖、哪些是死胡同，给出直觉建议作为系统下一轮迭代的指令 |
背景上，合作起点可追溯到 2025 年：书生-S1 在全国中学生数学奥林匹克（CMO）决赛的 AI 测试中取得 102 分、远超 78 分金牌线。此后上海AI实验室探索把模型能力从"竞赛级"升级到难度更高的"研究级"数学，与长期研究该猜想的许地生教授一拍即合。联合团队还同步搭建了面向数学研究场景的 Harness 系统。
✅ 为什么"通过 Lean 验证"是关键
AI 给的证明，凭什么信？答案是形式化验证。
北京大学董彬教授、刘若川院士团队用自主研发的 SHEAF 框架，完成了论文全部 4 个主定理的形式化验证，证明通过 Lean 检验。Lean 是一个交互式定理证明系统，能对形式化证明做严格的逐行逻辑检查。
换句话说：这套证明不仅能被人读懂，还能被计算机逐行验证，"照单全收"地确认逻辑完整、无漏洞、完全成立。
🧭 这意味着什么
一句话：AI 正在从"数学竞赛选手"变成"科研合作者"。
- 对科研范式：传统数学研究依赖个人天才的漫长摸索，这次把专家直觉系统性接入机器求解回路，形成"系统探索—专家判断—成果积累—反馈修正"的闭环，可复制到更多"搜索空间巨大、专家稀缺"的基础研究领域。
- 对国产大模型：在 IMO-Proof、AdvancedMathBench 等强调长程严谨推理的基准上，书生-S2 整体领先现有开源模型，部分指标超过 Gemini 3.1 Pro 等顶尖闭源模型，跻身全球长程推理能力最强的开源模型之列。
- 对普通读者：不必懂复动力系统也能 get 到重点——过去"AI 解世界级数学难题"多半还要打问号，这次的关键是"人机协同 + 机器可验证"，把成果钉死在可检查的地基上。
📋 相关论文与代码在哪里找？
- 论文标题：Codimension-one holomorphic Anosov diffeomorphisms，已在 arXiv 预印本平台发布
- 形式化代码：GitHub 仓库
frenzymath/HolomorphicAnosov（公开）
本文由加装AI助手整理发布 | 一手来源：上海人工智能实验室官方（2026-10-15）