书生-S2 人机协同完成三维 Ghys 猜想证明，并通过 Lean 形式化验证

书生-S2大模型人机协同完成三维Ghys猜想证明并通过Lean验证，产出约55万行代码。

据雷锋网 10 月 15 日报道，上海人工智能实验室访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型 S2（书生-S2），基于「通专融合」技术路径，通过人机协同完成了三维 Ghys 猜想证明。攻关过程中书生-S2 先后完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出上千页严密推导；北京大学董彬教授、刘若川院士团队随后用其自研 SHEAF 框架对论文全部四个主定理完成形式化验证，证明已通过 Lean 检验，全程约 5 天、峰值并发达 100 个智能体、产出约 55 万行 Lean 代码。相关论文已在 arXiv 发布，形式化代码在 GitHub 公开，可公开复核。需要说明的事实边界：该证明系人机协同完成而非模型独立完成，「中国科学家首次用中国大模型攻克世界级数学难题」为业内人士评价，未经独立证实。事件处于已落地阶段。

rss · 雷锋网 · 10月15日 07:14

「为什么重要」 Ghys 猜想由法国数学家Étienne Ghys 于 1995 年提出，被动力系统领域专家公认为该领域最重要的长期公开问题之一，此次 AI 深度参与其证明并通过严格形式化验证，是 AI for Science 路线在研究级数学上的一个标志性案例。已证实的是：书生-S2 在 IMO-Proof、AdvancedMathBench 等长程推理基准上整体领先现有开源模型，并在部分指标上超越 Gemini 3.1 Pro 等顶尖闭源模型；据雷锋网报道，动力系统专家谢俊逸曾用 GPT-6 尝试同一问题未找到证明方案（单方说法，未经独立证实）。接下来可盯的信号包括：论文与形式化代码经数学界同行的进一步审读结果，以及书生-S2 能力是否会以开源权重等形式开放。

「背景」 Ghys 猜想的核心是混沌动力系统行为能否决定几何分类，其实数版本的类似断言仍是完全公开的难题。许地生长期研究该猜想，曾与导师、菲尔兹奖得主 Avila 合作研究三维情形但未形成证明思路，后与学生张洁松合作取得部分弱相关结果并发表于《欧洲数学会杂志》（JEMS）。2026 年 3 月许地生成为上海 AI 实验室访问学者，双方组建联合团队并搭建面向数学研究的 Harness 系统；8 月内部迭代成型的书生-S2 在首轮推理中即产出 400 页推导报告，团队称其采用异步长程推理强化学习与 Harness 能力反向蒸馏的自进化算法（公司口径，细节以论文为准）。

查看原文 ↗