丘成桐弟子带着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 流后不久，丘成桐就向他指出，这个流会在空间细的地方把它勒断，这可能正是证明的第一步。Chow 后来和 Hamilton 合写过论文，又写了一整套 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 帮着拿下的，可能就是一道至今没人证出来的难题。
相关链接