书生-S2大模型攻克三维Ghys猜想，开启AI辅助数学研究新范式

事件概述

上海人工智能实验室访问学者、大湾区大学教授许地生团队，依托“书生”科学多模态大模型S2（书生-S2），基于“通专融合”技术路径，通过人机协同完成了三维Ghys猜想的证明。北京大学董彬教授、刘若川院士团队使用其开发的SHEAF框架对成果进行了形式化验证，确认其正确性。相关论文已在arXiv发布，形式化代码在GitHub公开。这是中国科学家首次以中国大模型攻克世界级数学难题。

核心信息

1. 关于Ghys猜想

• 背景：由法国数学家Étienne Ghys于1995年提出，是动力系统领域最重要的长期公开问题之一。
• 核心内容：探讨混沌的动力系统行为能否决定几何分类。若成立，混乱的动力学轨迹可化归为简洁的标准代数模型。
• 难度：复数情形比实数版本更具刚性，极难证明。此前包括GPT-6在内的其他模型尝试均未找到证明方案。

2. 技术路径与突破

• 模型能力：书生-S2具备大规模递归推理能力与高灵活的人机交互能力。针对该猜想的首轮推理即产出400页推导报告。
• 训练策略：坚持“通专融合”，在大规模科学知识预训练基础上，构造研究级后训练数据。突破异步长程推理强化学习，解决误差累积、状态维护等难题。
• 基准表现：在IMO-Proof、AdvancedMathBench等强调长程严谨推理的基准上，书生-S2整体领先现有开源模型，部分指标超越Gemini 3.1 Pro等顶尖闭源模型。

3. 人机协同攻关过程

• 分工模式：AI负责长链条大规模推演、拆解命题及生成多种思路；研究人员把握方向、判断死胡同并提供直觉建议。
• 具体进展：书生-S2完成7批接续推演，问题图从15个节点扩展至389个，输出上千页严密推导及数十种全新论证思路。
• 专家评价：国际前沿学者评价其“思考深度远超预期”。

4. 形式化验证

• 验证团队：北京大学董彬教授、刘若川院士团队。
• 工具与方法：使用自主开发的SHEAF框架，将命题组织为有向无环图，编排多个智能体并行工作。
• 结果：仅用约5天，峰值并发100个智能体，产出约55万行Lean代码，完成全部四个主定理的形式化验证，确认语义一致。

值得关注

• 科研范式变革：本研究验证了“系统探索—专家判断—成果积累—反馈修正”的新闭环范式，有望推广至更多搜索空间巨大且专家稀缺的基础研究领域。
• 历史对比：北大数学团队早在2021年便布局AI for Math，此前已实现国内首例依托AI自主突破重大数学猜想（安德森猜想），近期又独立完成了庞加莱猜想的形式化验证。本次成果进一步巩固了中国在该领域的领先地位。