新智元报道 刚刚，千禧年难题庞加莱猜想的完整证明，被整个写成了代码！ 干成这件事的，只是一个四人小团队。 带头的是丘成桐的弟子，一位研究了几十年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个多月。 半小时后，人类负