丘成桐弟子带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连黎曼几何最基础的工具都还不全。