首次国产大模型攻克世界级数学难题！北上广三地联手

闻乐 发自 凹非寺
量子位 | 公众号 QbitAI

一道困扰数学界30多年的猜想，被中国数学家和国产大模型联手拿下了！

大湾区大学许地生教授团队与上海AI实验室合作，借助书生-S2科学基础模型，证明了1995年提出的Ghys猜想在复余维一情形下成立，由此解决了悬而未决30多年的复三维情形。

现在，北京大学董彬教授、刘若川院士团队接棒，完成了这项成果的形式化验证工作。

这是中国科学家首次用中国大模型攻克世界级数学难题。

相关论文已上传arXiv，形式化验证代码也已公开。

中国团队攻克复流形Ghys猜想

1995年，法国数学家Étienne Ghys提出了一个关于动力系统与复几何结构的问题。

其中涉及的Anosov动力系统，有一个典型特点：系统演化时，一些方向上的距离不断被拉大，另一些方向则持续被压缩。

Ghys想弄清楚，在满足特定条件的复流形上，这类动力系统是否必然对应某种规整的代数结构。

复二维情形此前已有结果，但复三维情形一直没有得到完整证明。

而这次，大湾区大学许地生教授团队证明了Ghys猜想在复余维一情形下成立，也由此解决了悬而未决的复三维情形。

这次合作之前，团队已经围绕相关问题研究多年。

许地生教授就曾与其导师、菲尔兹奖得主Artur Avila研究过三维情形；

后来又与学生张洁松博士继续推进相关工作，并在《欧洲数学会杂志》（JEMS）发表过阶段性成果。

张洁松现就职于瑞典皇家理工学院，Ghys猜想是他从攻读博士至今一直关注的问题。

转机出现在AI开始参与数学研究之后。

2025年全国中学生数学奥林匹克决赛，上海AI实验室的书生-S1参加AI测试，取得102分，超过当年的78分金牌线。

当时模型给出的一些解题思路，引起了数学专家的注意。

2026年初，许地生团队与上海AI实验室展开合作，尝试让AI参与这项研究。

到了8月，书生-S2开始围绕猜想进行大规模推演。

第一轮，就交出了一份400页报告。

报告里有大量推导和不同的论证方向，但这些内容还需要数学家逐一判断。

随后团队把检查结果和新的问题反馈给模型，再进行下一轮推演。

就这样，双方进行了7批接续推演。

最初的问题图只有15个节点，后来扩展到389个节点。

累计生成的材料超过上千页，包含数十种论证思路。

经过多轮研究，团队形成了完整的证明。

最终，论文给出了复余维一全纯Anosov微分同胚的分类结果。

证明在相应条件下，这类系统与复环面上的双曲自同构双全纯共轭，复三维情形也因此得到解决。

而论文完成之后，另一支团队开始处理接下来的工作，把这些数学论证转换成形式化证明。

5天完成55万行Lean代码验证

北大董彬教授、刘若川院士团队是国内数学交叉与算术几何领域的顶尖力量。

刘若川是算术几何方向国际知名学者，任北大数院院长；

董彬则长期深耕AI与数学的交叉研究，是国内推动机器形式化证明的核心力量。

此次团队使用的是Lean 4定理证明系统，以及自研的SHEAF框架。

面对一份研究级数学证明，他们先将论文中的定义、命题和依赖关系整理成一张有向无环图；

然后，把不同的形式化任务分配给多个智能体处理；

完成之后，再将各部分组合起来，交给Lean检查。

这次工作用到的智能体，峰值并发数量达到100个。

从时间上看，证明论文9月29日首次上传arXiv，10月13日就已经完成了形式化验证。

约5天时间里，团队生成了约55万行Lean代码，最终完成了论文四个主要定理的形式化工作，包括Theorem A以及Theorem 1.1、1.2、1.3。

形式化证明代码目前已经公开在GitHub上。

30多年前Ghys提出的那个问题有了新的答案，人机协作也为数学研究打开了新的探索思路。

论文地址：https://arxiv.org/abs/2609.37695
形式化代码：https://github.com/frenzymath/HolomorphicAnosov