它一口气写了四百页，人只认下其中一行

2026-10-19 · 人工智能

10 月 15 日，上海人工智能实验室发了一篇新闻稿，标题很硬：「中国科学家首次用中国大模型攻克世界级数学难题」。

这种标题我一个月能见三次，本来打算划过去。让我停住的是里面一个不起眼的数字：首轮推理，四百页。

不是四百字，是四百页推导报告。一个模型坐在那里，对一个 1995 年提出、悬了三十一年的猜想，一口气写了四百页。

一、这道题难在哪

先把这个猜想说清楚，不然后面全是空的。

1995 年，法国数学家艾蒂安·吉斯（Étienne Ghys）在《Inventiones Mathematicae》上发了篇《Holomorphic Anosov systems》，末尾留了个猜测：每一个紧致复流形上的全纯 Anosov 系统，都双全纯共轭于某个复 infra-幂零流形上的全纯仿射自同构。

翻译一下。Anosov 系统可以想成揉面：按下去，往两边抻，再折回来。有的方向被拉长，有的方向被压扁。挨着的两个点，揉几下就分到天南地北。这就是混沌。

吉斯问的是：如果一个空间上能跑这种「既乱又完全规整」的运动，那这个空间本身长什么样？

他的答案是：只能长成晶体格子那样高度规整的样子。换句话说，运动乱到什么程度，反过来把空间的形状给锁死了。

他自己证了二维的情形。三维往上，卡住了。三十一年里没人推动。

这里有个技术上的槛，值得说一句：一个拓扑上等价于实环面的紧致复流形，在三维及以上，不一定是复环面。上面可以长出非标准的复结构。二维那套论证搬不过去，就卡在这儿。

二、人这边是谁

许地生，大湾区大学教授，上海 AI 实验室访问学者。做动力系统、谱理论、分形几何。他盯这个猜想很久，还跟自己的导师、菲尔兹奖得主阿图尔·阿维拉（Avila）一起试过三维，没走通。

张洁松，许地生的学生，现在在瑞典皇家理工学院做博后。Ghys 猜想是他从读博士第一天起就惦记的题，卡在几个具体的点上，卡了很多年。

另一头是模型。2025 年全国中学生数学奥林匹克决赛首次设了 AI 测试，三家国产大模型跟人类选手同场、同时间、同一套评分标准。书生-S1 考了 102 分，金牌线 78。阅卷专家的评语是：「答案表达方式非常接近人类」「一个新的解法，巧妙的调整法，在学生的解法中没有见过」。

就是这句「没有见过」，把事情推到了下一步。2026 年初，上海 AI 实验室和许地生的团队正式合作，目标从竞赛级数学转到研究级数学。

三、四百页里，人挑了什么

7 月底，许地生感觉模型变了。「系统开始变得更强了」。他把 Ghys 猜想也丢了进去。

然后就是那四百页。

我最好奇的其实是这一段：四百页里，多少是有用的？

官方给的说法很克制：其中有一些很有启发性，也有一些思路走不通，需要人来做进一步筛选和提示。张洁松的说法更实在——模型在跨领域知识的积累上比人广，输出了不少他不熟悉的、来自微分几何的观点和思路。

接下来的过程有点像淘金。团队从报告里抓住几个关键突破口，把方向校准，再喂回去。模型接着推。前前后后七批接续推演，问题图从 15 个节点长到 389 个，输出总量到了上千页，中间冒出几十种全新的论证思路。

最后拼出了完整的证明链条。

我不想把这件事写成「AI 独立解题」。它没有。真实的分工是这样的：模型负责铺开，把能想到的路全走一遍，走错的也写下来；人负责认路，看一眼就知道哪条能通、哪条是死胡同。

四百页的价值不在于它对，在于它够多。多到里面一定藏着一条人没想过的路。

四、验证这一步，比证明更像工程

数学界现在对 AI 参与的结果有个固定的追问：你怎么知道它是对的？

这次回答得比以往都硬。北京大学董彬教授、刘若川院士的团队接手，用自研的 SHEAF 框架做形式化验证，全部四个主定理都过了一遍 Lean。

Lean 是个定理证明器，你给它一段形式化证明，它逐行检查逻辑，错了就报错，不认人情。

数字是这样的：整个过程约 5 天，峰值 100 个智能体并行，产出约 55 万行 Lean 代码。整个仓库没有 sorry（Lean 里占位用的「此处待证」）。

但有一条必须说清楚，而且中文报道基本没提。

这个仓库的 README 自己写着：四个主定理里，有三个把 HomotopyTorusRigidity 当作前提假设。这是 Borel 猜想在环面情形下的版本，1969 年由 Hsiang 和 Wall 证过，是经典结果，用它是合理的。但严格讲，那三个定理是在这个前提下被机器检查通过的，不是无条件通过。第四个定理（Theorem 1.2）没有用这个假设。

这不是丑闻，数学论文引经典结果是常态。只是当标题写着「攻克」的时候，读者有权知道机器到底检查了什么。

还有一件事也得说：论文在 arXiv 上，还没过同行评审。9 月 29 日挂的 v1，10 月 13 日改到 v3。

五、作者栏里只有一个名字

我去翻了 arXiv 页面。2609.37695，作者一栏，一个人：Jiesong Zhang。

四百页推导、七批推演、389 个节点、55 万行 Lean 代码、100 个并行的 agent，最后署名的是一个人。

这不是抢功。论文里有「AI 使用声明」，原文写着：作者使用内部版本的书生-S2，通过多轮对话协助发展本文的数学思想与论证；作者已独立验证全部数学论证，并对稿件承担全部责任。

我读这段的时候想了一会儿。这大概是现阶段人机关系最诚实的一种写法：模型是工具，署名的人负责。数学界只认能站出来负责的那个。

还有个插曲，我很喜欢。论文上传之前，动力系统专家、北京大学谢俊逸教授收到了稿子。他听说这是国内模型做出来的，很好奇，特意拿 GPT-6 试了一遍同一个问题。

没做出来。

谢俊逸对猜想本身的评价倒是很冷静：「Ghys 猜想的难点在于其对应的实（数）版本的类似断言仍是著名的完全公开的难题，复数的情形问题变得更加刚性，是复动力系统刚性现象研究中的重要问题，非常困难。」

六、最后

许地生和张洁松在这道题上耗的时间，比模型多得多。模型那四百页，前后是几轮对话；人的那几年，是没法压缩的。

1995 年到 2026 年，三十一年。张洁松从读博开始盯这个题，盯到自己成了博后，题还在那儿。

我不太想讨论「AI 会不会取代数学家」。这次的事情太具体了，具体到没法拿来做宏大叙事：一个模型写了四百页，一个人翻到其中某一页，指着一行说，从这里往下走。

那一行，他认了六年。

信源：上海人工智能实验室新闻稿（2026-10-15）；arXiv:2609.37695（v1 2026-09-29，v3 2026-10-13）；形式化代码 github.com/frenzymath/HolomorphicAnosov；央广网 2026-10-18 专访。