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

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

带头的是丘成桐的弟子，一位研究了几十年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