精华速览

上海人工智能实验室访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型 S2，以“通专融合”路径通过人机协同完成三维 Ghys 猜想证明。该猜想由法国数学家 Étienne Ghys 于 1995 年提出，被公认为复动力系统领域最重要的长期公开问题之一。攻关中，书生-S2 完成 7 批接续推演，问题图从 15 个节点扩展至 389 个，输出上千页推导并生成数十种新论证思路。北京大学董彬教授、刘若川院士团队利用 SHEAF 框架，约 5 天完成全部四个主定理的形式化验证，峰值并发达 100 个智能体，产出约 55 万行 Lean 代码。相关论文已发布于 arXiv，形式化代码在 GitHub 公开。

要点透视

  • 三维 Ghys 猜想由法国数学家 Étienne Ghys 于 1995 年提出，核心是混沌动力系统行为能否决定几何分类，被动力系统领域专家视为该领域最重要的长期公开问题之一。
  • 上海 AI 实验室访问学者、大湾区大学教授许地生团队与上海 AI 实验室组建联合团队，依托书生-S2 及面向数学研究场景的 Harness 系统完成证明。
  • 书生-S2 针对三维 Ghys 猜想首轮推理即产出 400 页推导报告；攻关期间完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出总量达上千页。
  • 北京大学董彬教授、刘若川院士团队使用自主开发的 SHEAF 框架完成全部四个主定理的形式化验证，证明通过 Lean 检验，过程约 5 天，峰值并发达 100 个智能体，产出约 55 万行 Lean 代码。
  • 书生-S2 在 IMO-Proof、AdvancedMathBench 等长程严谨推理基准上整体领先现有开源模型，部分指标超越 Gemini 3.1 Pro 等顶尖闭源模型。
  • 相关论文已在预印本平台 arXiv 发布，形式化代码在 GitHub 公开。
  • 许地生曾与其导师、菲尔兹奖得主 Artur Avila 合作研究三维情形未形成有效证明思路，后与其学生张洁松在三维情形取得部分弱相关结果，刊发于《欧洲数学会杂志》。
  • 上海 AI 实验室计划将本次能力闭环封装为书生·端砚科学发现平台可复用的数学验证模块，形成“突破—封装—复用—再突破”的自进化飞轮。

文章拆解

三维 Ghys 猜想的证明之所以受到关注，首先在于问题本身的难度与标志性。它试图回答混沌动力系统行为能否决定几何分类，若成立，复杂动力学轨迹可化归为规整的代数模型。该猜想对应的实数版本类似断言仍是公开难题，复数情形因刚性更强而更加困难。许地生此前与菲尔兹奖得主 Artur Avila 合作研究三维情形未获有效证明思路，后与学生张洁松取得部分弱相关结果并刊发于 JEMS，说明该问题长期缺乏完整突破路径。

本次攻关的核心逻辑并非让模型独立完成证明，而是将专家直觉系统性接入机器求解回路。书生-S2 及配套系统承担长链条大规模推演，铺开多条支线、拆解命题、生成海量尝试；研究人员负责判断方向、识别死胡同并给出直觉建议。7 批接续推演、389 个节点和上千页推导表明，模型的价值在于扩展搜索空间与承接繁琐推导，而数学家的判断力仍是收敛到有效证明的关键。这一“系统探索—专家判断—成果积累—反馈修正”的闭环，比单次模型输出更具可复制性。

形式化验证是本次成果可信度的重要支撑。北大团队约 5 天完成四个主定理的 Lean 检验，峰值 100 个智能体、约 55 万行代码，显示 AI 辅助形式化已具备相当并行规模。但需注意，形式化验证确认的是证明在给定陈述下逻辑严格正确，其前提是形式化陈述与论文主定理语义一致；专家已确认这一点，但动力系统领域原有形式化基础设施不足，此次补充了大量基础设施，后续复用与维护成本尚待观察。

从行业影响看，书生-S2 在长程推理基准上部分指标超越 Gemini 3.1 Pro，且谢俊逸教授曾用 GPT-6 尝试该题未找到证明方案，这被业内视为中国大模型参与前沿数学攻关的一个信号。不过，单一难题的成功不能直接推广为通用科研能力，模型在多大范围的研究级数学问题上稳定有效，仍需更多独立案例检验。上海 AI 实验室计划将能力封装为端砚平台模块并向同源学科扩展，若“突破—封装—复用—再突破”飞轮运转，可能改变基础研究中专家稀缺领域的协作方式；其潜在风险在于，过度依赖模型生成思路可能引入难以察觉的隐性错误，而形式化验证目前仍受限于基础设施覆盖范围和人工编排成本。

查看原文