闻乐 发自 凹非寺
量子位 | 公众号 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
一键三连「点赞」「转发」「小心心」
欢迎在评论区留下你的想法！
— 完 —
🌟 点亮星标 🌟
