丘成桐弟子带AI狂写470万行，庞加莱猜想证明首次被机器完整验证

千禧年难题庞加莱猜想的完整证明，如今已被全部转化为代码！

完成这项工作的，是一个仅由四人组成的小团队。

领衔者是丘成桐的弟子，一位在Ricci流领域深耕数十年的资深教授，冲在最前线的是一位刚毕业的本科生，身后则是一群昼夜不停运转的AI。

他们借助证明助手Lean，将Hamilton和佩雷尔曼的证明从头到尾编写完成，总代码量约470万行。

其中约270万行，是在最后两周内，在ChatGPT、Claude等AI的协助下突击完成的。

这470万行代码已全部通过Lean内核的验证，没有一处使用“sorry”来留待后续补全。

过去，一个重大证明要让数学界公认“无误”，需要同行花费数年时间逐页审阅。

但这一次，评判权交给了机器，编写证明的主力也变成了AI。

佩雷尔曼的毕生心血，竟然只占六分之一

我们将整个仓库下载后，顺着最终的庞加莱定理，找出了所有直接和间接引用的代码。

实际用到的包括14197个代码文件，约402万行，最长的一条引用链串联起353个文件。

其中，佩雷尔曼三篇论文对应的代码合计约66万行，仅占六分之一。

论文写得越简略，Lean中需要补充的代码就越多，第三篇论文仅7页，平均每页对应1.4万行代码。

第三篇中只用一句话提及的曲线缩短流——即让一条曲线一边缩短一边变圆——在Lean中写了7.6万行。

剩下的六分之五，全是佩雷尔曼在论文中默认“读者早已掌握”的基础数学，其中分析学约109万行，微分几何约77万行。

Ricci流是佩雷尔曼证明的核心工具，它能让空间中弯曲剧烈的区域逐渐变得平缓，原理类似热传导。

短时存在性就是一个典型例子。它指出，给定任何初始形状，Ricci流至少能向前流动一小段时间，论文中只需引用前人的结论。

但Ricci流方程在不同坐标系下描述方式会变，算不上标准的热方程。

1983年，DeTurck想出一个办法：先在方程中添加一项，将其改造成标准热方程，解出结果后再还原。

在Lean中，这个方法背后的Sobolev空间、谱理论等工具都得从零开始构建，仅这一个定理就动用了89万行代码。

佩雷尔曼的杀手锏是典范邻域定理。

该定理指出，在Ricci流中，曲率即将趋于无穷大的区域，其形状必定有规律可循。

要么是一段细长的圆管，称为“颈”，要么是圆管一端封闭，称为“帽”。

证明这一个定理，就需要272万行代码，占整条依赖链的三分之二。

一老一少背后，是AI在管理AI

领头的Ben Chow是UCSD的数学教授。1986年，他在普林斯顿获得博士学位，导师正是丘成桐。

Hamilton提出Ricci流后不久，丘成桐就向他指出，这个流会在空间狭窄处将其勒断，这可能正是证明的第一步。Hamilton后来专门回忆过此事。

Chow后来与Hamilton合著过论文，并撰写了一套完整的Ricci流专著，在这个方向上钻研了几十年。

当年力挺Ricci流路线的是丘成桐，四十年后，带队将这条路线的证明完整输入计算机的，是他的学生。

2025年秋天，这位几何老将与同行办起了Lean线上学习班，像初学者一样从头学习这门新工具。他的个人主页上至今保留着一栏，标题叫“我的一些幼稚想法”。

那时Mathlib连黎曼几何最基础的工具都还不完备。

于是，Chow、Ziyang Qin和UCSD的博士生Yuan Liao花了七个月时间，先编写了约200万行的基础代码。

冲在最前线的本科生就是Ziyang Qin。他今年5月刚从康奈尔大学毕业，博士学业尚未开始，仓库中一万一千多次提交，有7477次记在他的名下。

9月，普林斯顿的Ayush Khaitan带着拓扑工具加入，四人共同完成了最后两周的冲刺。

至于具体使用了哪些AI，Khaitan透露，主力是ChatGPT Astra，部分难度较大的章节交给了Claude Fable。

按照团队开源的工具包，AI系统的最上层是“领队”，即研究者直接对话的主会话，它不负责编写证明，只把控数学路线。

领队之下有一个长期在后台运行的“调度”智能体，负责拆分任务、分配任务和验收。真正动手编写证明、查找错误、查阅资料的，是一批完成单项任务后就退出的临时智能体。

人类作者位于整套系统的最顶端，负责选择定义、确定命题，确认Lean中证明出来的，正是数学家想要证明的内容。

冲刺期间，团队正按照拓扑学家Moise在1977年出版的一本教科书，逐节编写拓扑部分。

9月20日一早，Claude Fable 5.1以领队身份编写了一份任务分配单，将这部分拆解成四条并行的任务线，交给OpenAI的编程智能体Codex。

每条任务线只能修改自己名下的文件，完成后提交清单，由Claude验收后再合并。

最关键的规则是，绝不能为了能证明而削弱命题。如果发现命题是假的也算成功，给出反例就停下来报告。

到了晚上，领队重新排出一张计划表。按3到4条任务线并行估算，书中“公认最难”的几节需要6到10周，走到拓扑版庞加莱最快也要4个多月。

半小时后，人类负责人决定换一种方法，先搭建骨架。

也就是先把整段证明的结构搭建出来，暂时无法证明的步骤先用sorry占位，以便提前暴露接口不匹配的问题，再逐个审查、定稿、证明这些占位的命题。

这些骨架文件单独存放，不进入主库，因此成品中依然没有一个sorry。

9月23日，Ben Chow那边证明了第32节中的三块内容，负责验收的是Claude领队。编译和审计全部零报错后，这位带过16个博士的老教授提交的成果才被收入主库。

第二天，书中从25.2到34.1的一系列定理全部证明完毕。美东时间9月27日凌晨3点38分，拓扑版庞加莱完成证明，距离那张计划表排出来还不到一周。

缝合了一个世纪的“手术”

回到庞加莱猜想本身。

它是庞加莱在1904年提出的，意思是：一个有限、封闭的三维空间中，如果任何一根绳圈都能收缩成一个点，那么它就是一个三维球面。

这道难题拖延了近一百年，更高维度的版本早已被攻破，唯独三维版本一直难以解决。

直到2002年底至2003年，佩雷尔曼在arXiv上连续发表三篇论文，利用Ricci流打破了僵局。

Ricci流的思路是将空间逐步熨平。如果一个空间能这样被熨成处处均匀的圆形，那么它就是一个球面，猜想也就得到了证明。

麻烦在于，空间并不一定会乖乖变圆。

想象一个哑铃，两端是两个大球，中间连着一根细杆。

Ricci流一旦启动，细杆会越来越细，在有限时间内“啪”地一下被勒断。勒断那一点的曲率趋于无穷大，数学上称为“奇点”。

Hamilton在这一步上卡了很多年。佩雷尔曼则多了一条典范邻域定理，他知道即将出问题的地方只可能是“颈”或“帽”，于是拿出了手术刀。

做法是：在细管即将被勒断之前，从颈部中间剪开，将即将出问题的那一小段丢弃。

然后，在两个断口处各缝上一个标准形状的帽子，让Ricci流继续运行。

佩雷尔曼在第三篇论文中又证明，对于单连通空间来说，这样流动一段、做一次手术、再继续流动，整个空间会在有限时间内收缩到消失。

消失的每一块都是三维球面，按剪开的位置粘回去，得到的仍然是三维球面。

这三篇论文中许多关键步骤只写了结论，直到2006年，几组数学家先后撰写了数百页的详细版本，数学界才确认这份证明是成立的。

在这次仓库中，前面那402万行代码，最终都是为一个仅23行的文件服务的。

文件中的定理正是庞加莱猜想：任何紧致、单连通、没有边界的三维拓扑流形，都与三维球面同胚。

Ricci流只能在光滑的空间上运行，因此还需要Moise定理来搭建一座桥梁。

Moise在1952年证明，每个三维拓扑流形都能切割成一块块小四面体拼凑起来，再将拼缝处理光滑，从而获得光滑结构。

那23行代码的后半部分，做的就是“先修桥、再过河”：先用Moise定理获得光滑结构，再调用光滑版本的庞加莱猜想。

Moise这座桥比手术部分还要费力。负责它的PL拓扑代码——即用小块拼接方法研究空间的代码——有46万行，比手术部分多出将近一倍。

有数学家在帖子下提问，最后那几行能否直接一行调用光滑版庞加莱就完事。

Khaitan回答说，参数C和hC无法省略，因为Lean需要先确认这个流形有一套光滑的坐标。这两个参数，正是从Moise定理中获取的。

千禧年难题的终结，也是下一场革命的开始

一年前，自动形式化智能体Gauss花了三周时间编写了2.5万行代码，就已经是大新闻。

这一次，四个人加一群AI，两周内写出的代码量是它的一百多倍。

斯坦福数学家Jared Duker Lichtman转发时，连打了两个感叹号。

这支小队的分工，几乎就是未来数学研究的雏形。老将确定方向，年轻人带着AI一行行编写代码，正确与否最后由Lean的内核判定。

人类数学家的精力，正从一步步编写证明，转向判断该证明什么，以及找出AI写错的地方。

按照这个势头，下一次AI协助拿下的，可能就是一道至今无人证明的难题。爱游戏作为科技领域的观察者，也关注到了这一突破性进展。

参考资料： https://x.com/ayushkhaitan343/status/2104289939840176167 https://github.com/qinz1yang/differential-geometry https://github.com/qinz1yang/differential-geometry/pull/80 https://arxiv.org/abs/2608.21502 https://github.com/qinz1yang/auto-formalizing-skills https://mathweb.ucsd.edu/~bechow/LeanOnMe/ https://x.com/keithadler/status/2104340829401980938 https://www.math.inc/gauss

本文来自微信公众号 “新智元”（ID：AI_era），作者：ASI启示录，36氪经授权发布。