AI辅助团队用470万行代码证完庞加莱猜想

一个由数学家和人工智能组成的四人团队，完成了一项颠覆数学研究范式的工作：他们将千禧年难题庞加莱猜想的完整证明，全部转化为可被形式化验证工具Lean直接校验的计算机代码，总代码量达到470万行。

这支团队的核心成员包括研究Ricci流数十年的资深学者、丘成桐的弟子Ben Chow教授，以及刚从康奈尔大学毕业的本科生Ziyang Qin，后者承担了大量代码编写工作。整个证明的代码库从Hamilton和佩雷尔曼的原始工作出发，从头搭建完成，所有代码都通过了Lean内核的严格校验，没有留下任何需要后续补充的占位标记。

在整个开发周期中，最后两周的冲刺阶段产出了约270万行代码，其中大部分都是在AI工具的辅助下完成的，AI成为了代码编写的核心助力。

原始论文仅占总代码的六分之一

通过梳理整个代码仓库的依赖关系，团队最终使用的有效代码包含14197个文件，总计约402万行，最长的引用链覆盖了353个代码文件。其中，佩雷尔曼三篇标志性论文对应的代码仅约66万行，占总有效代码的六分之一左右。

佩雷尔曼的论文以简洁著称，这意味着在转化为形式化代码时需要补充大量细节：他的第三篇论文仅有7页，平均每页对应1.4万行补充代码。仅其中一句话提及的曲线缩短流理论，在Lean代码中就需要7.6万行来完整验证。

剩下的五分之四代码，都是佩雷尔曼在原始论文中默认读者已掌握的基础数学知识：包括约109万行的分析学代码，以及77万行的微分几何代码。

作为佩雷尔曼证明的核心工具，Ricci流的原理类似热传导，能够让空间中曲率较大的区域逐渐平缓。以短时存在性定理为例，原始论文仅需引用前人结论，但在Lean中，由于Ricci流方程在不同坐标系下形式不同，需要通过DeTurck技巧将其转化为标准热方程，这背后涉及的Sobolev空间、谱理论等工具，单独这一个定理就需要89万行代码来实现。

佩雷尔曼的关键突破之一是典范邻域定理，该定理指出，Ricci流中曲率即将趋于无穷大的区域，只会呈现两种规则形状：细长的圆管（称为“颈”）或者一端封闭的圆管（称为“帽”）。证明这一定理的代码就达到了272万行，占据了整个依赖链的三分之二。

人机协同的新范式：AI驱动的证明流水线

Ben Chow教授早在2025年就开始学习形式化证明工具Lean，当时主流的数学库连黎曼几何的基础工具都不完善。他和Ziyang Qin、UCSD的博士生Yuan Liao花了七个月时间，先搭建了约200万行的基础数学代码库。

9月，普林斯顿的Ayush Khaitan加入团队，带来了拓扑领域的专业工具，四人团队开始了最后的冲刺。根据团队公开的流程，AI系统分为多层架构：最上层是与人类研究者对话的智能体，负责把控整体数学方向；其下是长期运行的调度智能体，负责拆分任务、分配工作并验收成果；真正执行代码编写、纠错和资料查询的，则是完成任务后自动退出的临时智能体。

9月20日，AI领队生成了任务清单，将拓扑部分的证明拆分为四条并行任务线，交由编程智能体执行。团队制定了严格的规则：每条任务线只能修改指定文件，完成后提交验收，且绝对不能为了通过校验而削弱命题，即使发现命题不成立并给出反例也算成功。

最初的计划表显示，最难的章节需要6到10周，完成拓扑版庞加莱猜想至少需要4个多月。但团队调整了策略，先搭建证明的整体框架，将暂时无法完成的步骤用占位符暂时标记，后续再逐个补全。这些占位文件并未进入最终的主代码库，因此最终的470万行代码没有一处占位标记。

9月23日，Ben Chow教授完成了第32节的三个核心定理，由AI领队完成编译和审计，确认零报错后才将代码并入主库。次日，从25.2到34.1的一系列定理全部完成验证，美东时间9月27日凌晨3点38分，拓扑版庞加莱猜想的形式化证明正式完成，距离最初的任务清单生成仅用了不到一周时间。

百年难题的破解：从Ricci流到拓扑手术

庞加莱猜想由法国数学家庞加莱在1904年提出，其核心内容是：任何一个有限、封闭的三维空间，如果其中每一条闭合曲线都能连续收缩为一个点，那么这个空间必然与三维球面同胚。这一问题困扰了数学界近百年，高维版本的猜想早已被攻克，但三维的情况始终难以突破。

2002年底到2003年，佩雷尔曼在预印本平台发布三篇论文，首次提出用Ricci流来证明庞加莱猜想。其核心思路是通过Ricci流将空间逐步“熨平”，如果最终能将空间转化为处处均匀的球面，就证明了猜想。但这一过程中会遇到一个关键问题：空间中的细杆区域会在有限时间内被“勒断”，曲率趋于无穷大，形成数学上的“奇点”。

Hamilton在这一步骤上停滞多年，而佩雷尔曼借助典范邻域定理，准确预判了奇点只会出现在“颈”或“帽”区域，从而提出了拓扑手术的解决方法：在细管即将被勒断前，从中间剪开并移除危险区域，再在两个断口处缝合标准的“帽”状结构，让Ricci流可以继续运行。

佩雷尔曼在第三篇论文中证明，对于单连通空间，反复执行流和手术的步骤，最终整个空间会在有限时间内收缩消失，而每一块收缩得到的都是三维球面，将这些块按原位置拼接，最终得到的仍然是三维球面。由于佩雷尔曼的论文省略了大量细节，后续多位数学家花费数年时间补充了数百页的详细证明，才让数学界最终确认其工作的正确性。

在这次的形式化代码库中，402万行有效代码最终都服务于一个仅23行的核心文件，该文件直接陈述了庞加莱猜想的正式结论：任何紧致、单连通、无边界的三维拓扑流形，都与三维球面同胚。

由于Ricci流只能在光滑空间上运行，团队还需要借助Moise定理搭建桥梁：1952年Moise证明，每个三维拓扑流形都可以拆分为小四面体的拼接结构，通过处理拼接缝可以得到光滑结构。这部分的代码比手术部分的代码还要多近一倍。

有同行曾质疑是否可以直接调用已有的光滑版庞加莱猜想结论，但团队解释称，必须通过Moise定理获取流形的光滑坐标参数，这两个参数是验证过程中不可或缺的环节，因此无法直接跳过。

千禧年难题的终结，也是下一场革命的开始

一年前，自动形式化智能体仅用三周就完成了2.5万行代码的形式化工作，曾引发学界轰动。而这次的四人团队借助AI，在两周内完成了超过100倍的代码量，将形式化数学证明推上了新的台阶。

这种人机协同的模式，很可能成为未来数学研究的标准范式：资深学者负责确定研究方向和核心命题，年轻研究者带领AI完成具体的代码编写和验证工作，最终的正确性则由形式化工具的内核来严格校验。

人类数学家的工作重心正在从一步步手写证明，转向判断应该证明什么命题，以及识别AI生成代码中的错误。按照当前的发展速度，下一次AI辅助攻克世界级数学难题的时刻，或许已经不远了。