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

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

领衔者是丘成桐的弟子，一位钻研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后来专门回忆过此事。

他后来与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，两周写出的代码是它的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氪经授权发布。