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

就在近日，千禧年大奖难题之一——庞加莱猜想的完整证明，被成功转化为计算机代码！

完成这一壮举的，是一个仅有四人的小型团队。

领衔的是丘成桐的弟子，一位钻研Ricci流数十年的资深教授，冲在最前线的则是一名刚毕业的本科生，身后是一群全天候轮转的人工智能。

他们借助证明助手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是加州大学圣地亚哥分校的数学教授。1986年，他在普林斯顿大学获得博士学位，导师正是丘成桐。

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

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

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

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

当时，Mathlib连黎曼几何最基础的工具都还不完善。

于是，Chow、Ziyang Qin和加州大学圣地亚哥分校的博士生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，在两周内写出的代码量是它的100多倍。

斯坦福大学的数学家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氪经授权发布。