国产大模型首破30年数学猜想，北上广三地联手攻克Ghys难题

一道困扰数学界30多年的猜想，被中国数学家和国产大模型联手拿下。大湾区大学许地生教授团队与上海AI实验室合作，借助书生-S2科学基础模型，证明了1995年提出的Ghys猜想在复余维一情形下成立，由此解决了悬而未决30多年的复三维情形。北京大学董彬教授、刘若川院士团队接棒，完成了这项成果的形式化验证工作。这是中国科学家首次用中国大模型攻克世界级数学难题。相关论文已上传arXiv，形式化验证代码也已公开。

1995年，法国数学家Étienne Ghys提出了一个关于动力系统与复几何结构的问题。其中涉及的Anosov动力系统，有一个典型特点：系统演化时，一些方向上的距离不断被拉大，另一些方向则持续被压缩。Ghys想弄清楚，在满足特定条件的复流形上，这类动力系统是否必然对应某种规整的代数结构。复二维情形此前已有结果，但复三维情形一直没有得到完整证明。这次，许地生团队证明了Ghys猜想在复余维一情形下成立，也由此解决了复三维情形。

合作之前，团队已围绕相关问题研究多年。许地生曾与其导师、菲尔兹奖得主Artur Avila研究过三维情形，后来又与学生张洁松继续推进，并在《欧洲数学会杂志》发表过阶段性成果。张洁松现就职于瑞典皇家理工学院，Ghys猜想是他从攻读博士至今一直关注的问题。

转机出现在AI开始参与数学研究之后。2025年全国中学生数学奥林匹克决赛，上海AI实验室的书生-S1参加AI测试，取得102分，超过当年的78分金牌线，其解题思路引起数学专家注意。2026年初，许地生团队与上海AI实验室展开合作，尝试让AI参与研究。到了8月，书生-S2开始围绕猜想进行大规模推演，第一轮就交出一份400页报告，包含大量推导和不同论证方向，但需数学家逐一判断。随后团队把检查结果和新问题反馈给模型，再进行下一轮推演。双方共进行7批接续推演，最初的问题图只有15个节点，后来扩展到389个节点，累计生成材料超过上千页，包含数十种论证思路。经过多轮研究，团队形成了完整证明。最终论文给出复余维一全纯Anosov微分同胚的分类结果，证明在相应条件下，这类系统与复环面上的双曲自同构双全纯共轭，复三维情形也因此得到解决。

论文完成后，北大董彬教授、刘若川院士团队开始把数学论证转换成形式化证明。刘若川是算术几何方向国际知名学者，任北大数院院长；董彬长期深耕AI与数学交叉研究，是国内推动机器形式化证明的核心力量。此次团队使用Lean 4定理证明系统及自研SHEAF框架，先将论文中的定义、命题和依赖关系整理成有向无环图，再把不同形式化任务分配给多个智能体处理，完成后组合起来交给Lean检查，智能体峰值并发数量达到100个。论文9月29日首次上传arXiv，10月13日完成形式化验证，约5天时间生成约55万行Lean代码，完成论文四个主要定理的形式化工作，包括Theorem A以及Theorem 1.1、1.2、1.3。形式化证明代码已在GitHub公开。