上海AI实验室用书生-S2人机协同证明三维Ghys猜想

上海人工智能实验室宣布，访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型S2，基于通专融合技术路径，通过人机协同完成三维Ghys猜想的证明。该猜想由法国数学家Étienne Ghys于1995年提出，涉及紧致复流形上全纯Anosov系统的分类问题，被动力系统领域视为长期公开难题。北京大学董彬教授、刘若川院士团队利用自主开发的SHEAF框架完成论文全部四个主定理的形式化验证，证明通过Lean检验。 合作起点可追溯到2025年全国中学生数学奥林匹克决赛首设的AI测试，书生-S1取得102分，超过78分金牌线并在参评国产大模型中排名第一。2026年初双方正式启动模型训练合作，同步搭建面向数学研究场景的Harness系统。训练上，团队在大规模科学知识预训练基础上构造研究级后训练数据，并突破异步长程推理强化学习训练方法，解决误差指数级累积、长期状态维护、自我纠错等问题，还将Harness带来的能力提升反向蒸馏回模型。 针对三维Ghys猜想，书生-S2首轮推理即产出400页推导报告，此后完成7批接续推演，问题图从15个节点扩展到389个，输出总量达千页，并生成数十种全新论证思路。研究人员负责判断思路价值、校准探索方向，模型承担大规模支线推演，形成多轮人机交互闭环。团队称书生-S2在IMO-Proof、AdvancedMathBench等基准上整体领先现有开源模型，部分指标超过Gemini 3.1 Pro。 形式化验证方面，北大团队用SHEAF框架将论文命题、定义及依赖关系组织成有向无环图，多个智能体并行推进，整个过程约5天，峰值并发达100个智能体，产出约55万行Lean代码。由于动力系统领域原有形式化基础设施不足，此次还补充了大量覆盖论文依赖文献结果的基础设施。 论文Codimension-one holomorphic Anosov diffeomorphisms已在arXiv发布，形式化代码在GitHub公开。上海AI实验室表示，后续将把本次跑通的能力闭环封装为书生·端砚科学发现平台可复用的数学验证模块，并把推理能力扩展至数学结构同源的其他学科，形成突破、封装、复用、再突破的迭代路径。