困扰数学界30余年的世界级难题——三维Ghys猜想，迎来了破解时刻。10月15日，上海人工智能实验室宣布，其访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型S2（书生-S2），基于"通专融合"技术路径，通过人机协同完成了三维Ghys猜想的完整证明。相关论文已在预印本平台arXiv发布，形式化验证代码同步在GitHub公开。
人机协同：不是替代，而是结对
这次证明最值得玩味的不是"AI做出了数学发现"，而是协作模式。书生-S2走的是"通专融合"路径：通用大模型的语言与推理能力，加上针对科学问题的专用训练，让模型能够在高维几何与动力系统的证明链条中提出引理、补全推导、排查反例。人类数学家则负责把握证明的整体架构、提出关键洞察、裁决每一步的数学合法性。模型负责在庞大的搜索空间里不知疲倦地试探，人负责在关键岔口做判断。
这种分工恰恰回应了"AI能否做原创数学"的争论。纯粹让模型端到端输出证明，既不可靠也难以验证；纯粹人工推进，又受限于组合爆炸的搜索空间。人机协同把证明过程拆解成可检验的中间产物——每一步引理都可以被独立审视、被形式化工具复核，这正是数学共同体能够接受的严谨性标准。
形式化验证：给证明上第二道保险
北京大学董彬教授、刘若川院士团队用自主开发的SHEAF框架对本次证明完成了形式化验证。形式化验证的意义在于：它把自然语言写成的证明翻译成机器可机械检查的逻辑链条，任何隐藏的跳步、循环论证都会被无情揪出。近年来多起"证明撤回"事件——包括大模型辅助研究中出现的符号错误导致证明链条崩塌——都说明，形式化验证正在从可选项变成高风险证明的标配。
对国内科研生态而言，这次突破的象征意义大于单题本身。它证明了国产科学大模型已经具备支撑前沿数学研究的能力，而"模型+形式化验证"的双轮架构，为AI for Science提供了一条可复制的工程路径：模型负责探索的广度，验证负责结论的硬度。
下一步：从单题突破到方法论
真正的考验在后面。三维Ghys猜想的解决方式能否迁移到其他长期悬置的猜想？人机协同的流程能否沉淀为数学家日常可用的工具链？书生-S2的这次亮相，更像是一次能力宣言：科学大模型的竞争，已经从刷基准榜单，进入了"能不能啃下硬骨头"的实战阶段。数学界接下来会用更挑剔的眼光审视每一步证明——而这，恰恰是科学进步最健康的姿态。