10月15日，上海人工智能实验室宣布：困扰数学界30余年的世界级难题——三维Ghys猜想，由该实验室访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型S2（书生-S2），以人机协同的方式完成证明，并通过形式化验证。这是官方首次公开国产大模型深度参与世界级数学难题完整研究流程的案例。
先解释这条新闻的主角。书生-S2是上海人工智能实验室面向科学研究的科学多模态大模型，定位于把文本、公式、图表等多形态科学信息统一处理，服务科研全流程。三维Ghys猜想则是低维拓扑与动力系统交叉领域的知名难题，由法国数学家Étienne Ghys在20世纪80年代提出，涉及纽结与周期轨计数关系的普适规律，30余年来一直缺乏完整证明。
研究方式： 据披露，书生-S2在研究流程中承担了推导辅助、结构搜索与验证支撑等环节，数学家负责提出问题、构建框架与把关方向，大模型负责在海量变换与组合空间中做系统性探索，最终成形的证明通过形式化验证——也就是用计算机程序逐行检查每一步逻辑是否严格成立，排除了「论文看着对、细究有漏洞」的传统风险。
这项成果放在近一年的AI数学脉络里看更有分量。今年9月，OpenAI宣称其智能体在千禧年难题上取得进展，随即引发25位菲尔兹奖得主联署抗议，学界对「AI生成证明无法核验」的担忧集中爆发；上个月还有AI一次批量产出722篇数学论文的消息引发震动。争议的焦点从来不是AI算得快不快，而是结果可不可信。书生-S2这次选择的路径恰好回应了这一痛点：证明由人机协同完成，且以形式化验证收口，可信度有硬性保障。
对国内AI科研生态而言，这个案例的标杆意义在于「进入流程」四个字——大模型不再是查资料、写摘要的外围工具，而是进入了提出猜想、搜索结构、验证证明的科研主链路。上海人工智能实验室近年持续押注科学大模型方向，书生系列在气象、药物、材料等领域已有落地，数学是其中对严谨性要求最苛刻的试金石。
需要说明的是，该成果的完整论文与验证代码的公开范围、以及国际数学界对证明细节的同行评议进展，官方通报尚未给出细节，后续值得跟进。但方向已经清楚：AI与数学的关系，正在从「批量刷题」走向「严谨共研」。