一道困扰数学界30多年的猜想，被中国数学家和国产大模型联手攻克。
大湾区大学许地生教授团队与上海AI实验室合作，借助书生-S2科学基础模型，证明了1995年提出的Ghys猜想在复余维一情形下成立，由此解决了悬而未决30多年的复三维情形。
随后，北京大学董彬教授、刘若川院士团队接棒，完成了该项成果的形式化验证工作。
这是中国科学家首次利用中国大模型攻克世界级数学难题。相关论文已上传arXiv，形式化验证代码也已公开。
中国团队攻克复流形Ghys猜想
1995年，法国数学家Étienne Ghys提出了一个关于动力系统与复几何结构的问题。其中涉及的Anosov动力系统具有典型特征：系统演化时，部分方向距离不断拉大，另一些方向则持续压缩。
Ghys旨在探究在满足特定条件的复流形上，这类动力系统是否必然对应某种规整的代数结构。此前复二维情形已有结果，但复三维情形一直未获完整证明。
此次，大湾区大学许地生教授团队证明了Ghys猜想在复余维一情形下成立，从而解决了这一难题。
深耕多年迎转机
在此次合作前，团队已围绕该问题研究多年。许地生教授曾与其导师、菲尔兹奖得主Artur Avila研究过三维情形；后与学生张洁松博士继续推进，并在《欧洲数学会杂志》（JEMS）发表阶段性成果。张洁松现就职于瑞典皇家理工学院，Ghys猜想是其从博士阶段至今持续关注的课题。
人机协作七轮推演
转机出现在AI参与数学研究之后。2025年全国中学生数学奥林匹克决赛中，上海AI实验室的书生-S1在AI测试中取得102分，超过当年金牌线，其解题思路引起数学专家关注。
2026年初，许地生团队与上海AI实验室展开合作。8月，书生-S2开始围绕猜想进行大规模推演。首轮即生成一份40页报告，包含大量推导和不同论证方向。团队对内容逐一判断后，将检查结果和新问题反馈给模型，进行下一轮推演。
双方共进行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