上海AI实验室：书生-S2 人机协同证明三维 Ghys 猜想，北大用 Lean 完成形式化验证

上海人工智能实验室 10 月 15 日公告：访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型 S2（书生-S2），以「人机协同」方式完成三维 Ghys 猜想的证明；北京大学董彬教授、刘若川院士团队用自研 SHEAF 框架完成形式化验证，四个主定理全部通过 Lean 检验。Ghys 猜想由法国数学家 Étienne Ghys 于 1995 年提出，问的是紧致复流形上的全纯 Anosov 系统能否被分类为复环面上的标准自同构——官方称它是动力系统领域的长期公开问题之一，也是检验数学推理能力的试金石。

官方给出的过程数字：针对该猜想的首轮推理，书生-S2 产出 400 页推导报告；攻关阶段完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出总量上千页，并生成数十种新论证思路。形式化侧：北大团队约 5 天完成验证，峰值并发 100 个智能体，产出约 55 万行 Lean 代码，专家确认形式化陈述与论文主定理语义一致。模型侧官方提到两条训练方法——异步长程推理强化学习，以及把 Harness 带来的能力增益反向蒸馏回模型的自进化算法。

两项要区分的事实。一是论文本体早于公告：arXiv 2609.37695《Codimension-one holomorphic Anosov diffeomorphisms》（作者张洁松，现就职于瑞典皇家理工学院）首版为 2026-09-29、本版 v3 为 2026-10-13，形式化代码仓同为 10-13 建立，故本条按机构公告日 10-15 收录，而证明的预印本公开已在 16 天前。二是 AI 的参与程度：论文正文（v3 HTML 全文）未检出 LLM 或 AI 协助字样，「首次用中国大模型攻克世界级数学难题」是上海AI实验室的公告口径，本站未见过独立第三方对该分工的核证。

原文链接：上海人工智能实验室