三十年的猜想，七轮对话，和五十五万行验算
先把一个数学问题说成大白话。想象一台搅拌机，里面的液体被反复拉伸、折叠再倒回，轨迹乱得像一团毛线。1995 年，法国数学家艾蒂安·吉斯（Étienne Ghys）问：在复流形上，这种乱到极致的全纯 Anosov 系统，是不是都能通过一个双全纯变换，化成某种规规整整的标准模型？乱麻理成直条，这就是 Ghys 猜想。它被…
先把一个数学问题说成大白话。想象一台搅拌机，里面的液体被反复拉伸、折叠再倒回，轨迹乱得像一团毛线。1995 年，法国数学家艾蒂安·吉斯（Étienne Ghys）问：在复流形上，这种乱到极致的全纯 Anosov 系统，是不是都能通过一个双全纯变换，化成某种规规整整的标准模型？乱麻理成直条，这就是 Ghys 猜想。它被动力系统领域公认为最重要的长期公开问题之一，是检验数学推理能力的试金石【直引：科技日报与科学网转述】。
乱麻理了三十一年，没人理得动。它对应的实数版本，至今仍是全球未解难题。
10 月 14 日，消息从大湾区大学与上海人工智能实验室传来：许地生教授团队依托书生科学多模态大模型 S2，以人机协同方式完成了三维 Ghys 猜想的证明；北京大学董彬教授与刘若川院士团队用自研框架做了形式化验证。这是中国科学家首次依托国产大模型攻克世界级数学难题【直引：央广网、科技日报】。论文题为《Codimension-one holomorphic Anosov diffeomorphisms》，9 月 29 日挂上 arXiv，10 月 13 日修订到第三版，新增了 AI 使用声明与形式化说明【直引：arXiv:2609.37695】。
🧮 证明到底证了什么
先把结论放准。论文证明：紧连通复流形上每一个余维为一的全纯 Anosov 微分同胚，都双全纯共轭于复环面上的一个双曲自同构。这验证了 Ghys 猜想在余维为一的情形，复三维是其中的特例【直引：论文摘要】。
这里有个容易被标题吞掉的限定：余维为一。猜想本身说的是所有紧致复流形，论文拿下的是其中一个切片。把猜想比作一栋楼，这次打通的是楼梯间，不是整层。至于猜想陈述里那个复 infra-幂零流形，在余维为一的情形下被收窄成了复环面，这个收窄本身就是证明的力量所在【推论：由论文陈述与媒体报道比对得出】。
🤝 七轮对话是怎么分工的
这场证明最值得看的不是结论，是流水线。
书生 S2 先后完成七批接续推演，问题图从 15 个节点扩展到 389 个，输出总量达千页严密推导，同时生成数十种全新论证思路。许地生与学生张洁松在 AI 给出的首轮探索里抓住关键突破口，持续给模型反馈、校准方向。用官方说法，专家直觉被系统性接入机器求解回路，形成"系统探索、专家判断、成果积累、反馈修正"的闭环【直引：科学网与南方+报道】。
一个对照实验值得记下。论文上传 arXiv 之前，北京大学谢俊逸曾用 GPT-6 挑战同一道题，没能找到证明方案【直引：科学网】。同为前沿模型，一个卡壳一个突破，差别不全在模型，也在人与机器怎么配合。
为什么非要机器验证不可？因为 AI 参与的长推导，错一步整条链就塌。北大团队的 SHEAF 框架用约五天时间，峰值一百个智能体并行运算，产出约五十五万行 Lean 代码，把论文全部四个主定理逐一形式化，确认形式化陈述与论文主定理语义一致，证明逻辑严格正确【直引：南方+报道】。针对动力系统领域形式化基础设施不足的老问题，团队还补写了一大批基础文献结果的形式化。
这串数字摊开看更直观。
形式化验证的几个尺度
| 项目 | 数字 | 说明 |
|---|---|---|
| 验证框架 | SHEAF | 北大董彬、刘若川团队自研 |
| 墙上时间 | 约 5 天 | 从接收到完成全部四定理 |
| 并行智能体峰值 | 约 100 个 | 大规模并行运算 |
| Lean 代码产出 | 约 55 万行 | 覆盖四个主定理及依赖文献 |
🎓 这条流水线的来路
书生模型的数学本事有明确的升级路径。2025 年全国中学生数学奥林匹克决赛首设 AI 测试，三家国产大模型与人类选手同时长答题、同标准阅卷，书生 S1 拿 102 分，在参评模型中排第一，远超 78 分的金牌线。拿到金牌后，上海 AI 实验室与许地生团队在 2026 年初正式启动合作，目标是把模型能力从竞赛级推向研究级【直引：科技日报】。
从竞赛题到研究级难题，中间隔着的不是难度，是答案的长度。竞赛题有标准解，研究级证明要自己开路。七批推演，389 个节点，千页推导，这些数字说的是同一件事：AI 在超长链条上不疲倦，人类在关键岔路口不糊涂。
⚠️ 三个需要说清的边界
第一，论文是预印本，未经同行评审。数学结论的最终确认，要等期刊与共同体的检验，不是等新闻稿。
第二，AI 的角色是辅助。首轮探索，大规模推演，数十种思路生成，由模型完成；突破口由人抓住，方向由人校准。把这项工作说成"AI 解决了数学难题"，是把人的判断从链条里抠掉【判断：依据官方通稿与人机分工描述】。
第三，实数版本仍未解决。这次拿下的是复情形的余维一切片，猜想的完整版还立在那里。许地生本人的说法也留着余地：这只是开端【直引：科学网】。
🧭 然后呢
回头看，这件事真正的产品不是那份证明，是那条流水线。七轮对话加五十五万行验算，把"专家直觉加机器求解"从口号跑成了可复用的闭环。北大团队已计划把跑通的能力封装成书生端砚科学发现平台的可复用数学验证模块【直引：南方+】。
下一次再遇到某个领域"搜索空间巨大而专家稀缺"的硬问题，可以问一句：这套闭环，迁得过去吗？
参考文献
- Jiesong Zhang, *Codimension-one holomorphic Anosov diffeomorphisms*, arXiv:2609.37695[v3], 2026-10-13. https://arxiv.org/abs/2609.37695
- 科技日报, *中国科学家首次用中国大模型攻克世界级数学难题*, 2026-10-15. https://www.stdaily.com/web/gdxw/2026-10/15/content_596583.html
- 科学网（赵广立）, *国内学者使用国产大模型攻克世界级数学难题*, 2026-10-15. https://news.sciencenet.cn/htmlnews/2026/10/572932.shtm
- 南方+, *困扰数学界 30 余年的世界级难题, 中国科学家联合国产大模型成功破解*, 2026-10-15. https://www.nfnews.com/content/Lownjg9B6J.html
- CGTN, *Chinese researchers solve 3D Ghys conjecture with homegrown AI model*, 2026-10-15. https://news.cgtn.com/news/2026-10-15/Chinese-researchers-solve-3D-Ghys-conjecture-with-homegrown-AI-model-1RgD8zQ3Z3a/p.html