书生-S2参与证明三维Ghys猜想，北大团队用形式化方法验了一遍

一道困扰数学界三十多年的问题，三维Ghys猜想，这次有了中国大模型参与完成的证明。

上海人工智能实验室访问学者、大湾区大学教授许地生团队，用书生科学多模态大模型S2（书生-S2）通过人机协同的方式完成了证明。实验室给这条技术路径的说法叫“通专融合”，大意是通用大模型和专业领域能力结合起来做。

光有证明还不够，数学界最在意的是对不对。北京大学董彬教授、刘若川院士团队用自己开发的SHEAF框架，对这份证明做了形式化验证，也就是把证明翻译成机器可以逐步检查的形式，确认每一步推理都成立。

论文已经发在arXiv上，形式化代码也在GitHub公开了。上海AI实验室称，这是中国科学家首次用中国大模型攻克世界级数学难题。

有个对照可以看：前阵子OpenAI一口气发出722份AI数学手稿，很快就有几篇因为符号错误撤回，引来不少数学家批评。这次的做法是先做形式化验证、再连代码一起公开，可信度上明显站得更稳。

AI做数学，接下来大概都得走这条路：证明是不是AI写的不重要，能不能被机器验过才重要。站内也收录了书生通用大模型体系，感兴趣可以看看这一系列模型。