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

新智元报道

刚刚，千禧年难题庞加莱猜想的完整证明，被整个写成了代码！

干成这件事的，只是一个四人小团队。

带头的是丘成桐的弟子，一位研究了几十年Ricci流的老教授，冲在最前面的是一个刚毕业的本科生，身后是一群24小时连轴转的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，两周写出的是它的一百多倍。

斯坦福数学家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

编辑：摩西