卡了 31 年的数学难题，被中国 AI 解出来了——但功劳簿该署谁的名字？

luyuanhong

卡了 31 年的数学难题，被中国 AI 解出来了——但功劳簿该署谁的名字？

原创  逆旅战士  AI 轻创研习社  2026 年 10 月 25 日 08:57  江苏

一个让全世界数学家挠头 31 年的猜想，上周被"铁三角"联手拿下了：一位中国数学家、一台国产大模型，外加一套专治"AI 吹牛"的机器验证系统。

事情很简单，又很不简单。

1995 年，法国数学家艾蒂安·吉斯（Etienne Ghys）抛出一个问题：一个混沌的动力系统，它的“行为”能不能反过来决定它的“几何形状”？听起来绕，翻译成人话就是——一团乱麻似的动态轨迹，能不能被归整成几个干净的标准化模型？

这个问题，学界叫它 Ghys 猜想，是动力系统领域公认最重要的长期公开问题之一，也是一块检验数学推理能力的“试金石”。三十一年里，无数聪明人碰过它，都没能证明。

直到 10 月 15 日，上海人工智能实验室发布消息：大湾区大学教授许地生团队，依托国产“书生”科学大模型 S2 ，用“人机配合”的方式，把这个猜想证了出来。

真正让人坐不住的，不是“ AI 又解了一道题”这个老套剧情，而是藏在背后的三个细节。

一、上千页推导，机器逐行查过，一个字没错

AI 能写上千页推导，不稀奇。稀奇的是，这上千页被人逐行查过，而且“一句错都没有”。

验证环节才是这次真正的门道。北京大学的董彬教授、刘若川院士团队，动手做了一套形式化验证：用 Lean 4 外加他们自研的 SHEAF 框架，把证明的四个主定理逐条喂给计算机。

什么叫形式化验证？普通数学证明靠的是“人类读者补条件”——你写一句“显然”“易证”，读者自己脑补剩下的二十步。形式化验证不行，每一步都得让计算机点头，含糊一个字都过不去。

结果：四个主定理，全过。

团队花了五天，峰值同时跑 100 个智能体并行推理，最后写出 55 万行 Lean 代码。这个数字本身不性感，性感的是它背后的意思——“能生成”和“可信”之间那道门槛，这一次第一次真的被跨过去了。

过去 AI 解数学题，最大的槽点就是“看起来对，但没法信”。这次，它过了机器这一关。

二、赢的不是算力，是“被真问题磨过”

另一个有意思的细节，是个反面参照。

据公开报道，在这次证明提交前，北京国际数学研究中心的谢俊逸教授，曾用 GPT-6 去啃同一道题——没找到方案。更早的时候，也有国际动力系统的专家，拿海外的模型试过这题，同样铩羽而归。

GPT-6 是什么量级的存在？闭源最强的旗舰之一。可它没解出来。

那“书生”S2 凭什么解出来了？答案是它的底子：所谓"通专融合"——把科学语料、专业任务和真实科研命题揉在一起训练。换句话说，这道题喂进去之前，它已经在真实数学场上跑过一轮了。

差距，正从“谁算得多”，变成“谁被真问题磨过”。

更有意思的是它的起点。书生模型最早在 2025 年全国中学生数学奥林匹克（CMO）的首次 AI 测试里，拿了 102 分——比 78 分的金牌线还高出不少。一个从“高考状元”一路杀进“科研攻关”的模型，这个成长路径，本身就挺耐人寻味。

三、决定从哪儿下手的，还是人

这才是整件事里我最想说的部分。

整个证明过程，实际是一场拔河。年初，许地生受聘为上海人工智能实验室访问学者，和团队搭了一套面向数学研究的 Harness 系统。7 月底他察觉模型能力出现质变，把猜想整个喂了进去。

首轮，书生 S2 交出 400 页报告。接下来就轮到人了：科研人员反复反馈、校准方向，书生 S2 先后完成 7 批接续推演，问题节点从 15 个一路长到 389 个，最终输出千页推导。中途，长期关注这个难题的张洁松博士从 AI 的推导里抓到了关键突破口。

看清楚这个协作模式了吗：

机器负责铺路，人负责选路。

100 个智能体跑了五天，但“从哪儿下手”这个决定，始终攥在人手里。

这跟半个月前地球另一边的另一份答卷，形成了微妙的对照。谷歌 DeepMind 的 AlphaProof Nexus 同期也发了一篇《科学》论文，在 353 个形式化数学问题里解出 9 个，其中 2 个悬了 56 年。它的打法是“无人驾驶”——机器自己找题、自己解、自己交卷，人退到评审席。

两条路，指向同一个结论：数学的发现方式，正在被改写。区别只是，中国人选了“人机协同”，美国人选了“机器单飞”。

结语：别急着喊“ AI 取代数学家”

老实说，看到这类新闻，朋友圈里最容易冒出来的两句话是——“数学家要失业了”和“ AI 又吹牛了”。

都不对。

先说“失业”这茬。许地生团队留下的，是一套能照着跑的工作流：摆出真问题、模型大规模递归推理、人挑路线、形式化系统过一遍。在这套流程里，AI 是提升“智力生产上限”的工具，人仍然是把控方向的关键角色。它取代的，是过去那种“靠天才个人苦熬十几年攒直觉”的苦功夫，而不是数学家本人。

再说“吹牛”。这次跟以往最大的不同，恰恰是它不靠吹——千页推导过了形式化验证这道硬门槛，这本身就是 AI 数学第一次真正意义上“可信”了一回。

所以，正确的打开方式也许是：这不是“ AI 抢了数学家的饭碗”，而是“数学家多了一台能同时铺开几百条路的机器”。

而那个被解开的 Ghys 猜想，其实也在提醒我们一句大实话——再聪明的机器，也得先有一个人，敢把三十年没人啃下的难题，喂进它的嘴里。

AI 轻创研习社