庞加莱猜想的完整证明，已经被一个 4 人团队写成了可由机器核验的代码。
这套形式化证明使用证明助手 Lean，把 Hamilton 和佩雷尔曼的证明从头到尾写成约 470 万行代码。其中约 270 万行是在最后两周借助 ChatGPT、Claude 等 AI 完成。全部代码都通过了 Lean 内核检查，没有留下任何「以后再证」的 sorry。
402 万行直接或间接支撑最终定理
据文中对仓库的梳理，沿着最终的庞加莱定理向上追溯，直接和间接引用到的代码共有 14197 个文件，约 402 万行，最长的一条引用链串起了 353 个文件。
其中，佩雷尔曼 3 篇论文对应的代码合计约 66 万行，只占六分之一。论文写得越简略，Lean 里需要补出的代码就越多。第 3 篇论文只有 7 页，平均每页对应约 1.4 万行代码。文中提到，第三篇里只用一句话带过的曲线缩短流，在 Lean 里写成了 7.6 万行。
其余六分之五主要是论文默认读者已掌握的基础数学内容，其中分析学约 109 万行，微分几何约 77 万行。
Ricci 流关键定理占据大部分依赖链
Ricci 流是佩雷尔曼证明的核心工具。文中将其比作热传导：空间里弯曲严重的部分会逐步变得平缓。
短时存在性是其中一个基础结论，即任给一个初始形状，Ricci 流至少能向前演化一小段时间。由于 Ricci 流方程在不同坐标下形式会变化，它并不是标准的热方程。1983 年，DeTurck 提出先给方程加上一项，把它改造成标准热方程，求解后再变回去。到了 Lean 里，这一方法背后的 Sobolev 空间、谱理论等工具都需要补齐，仅这一个定理就要用到 89 万行代码。
佩雷尔曼证明中的关键武器是典范邻域定理。它说明，在 Ricci 流中曲率即将趋于无穷大的区域，局部形状只能是「颈」或「帽」。文中称，证明这一个定理就要用到 272 万行代码，占整条依赖链的三分之二。
团队成员与 AI 协作方式
带队者是加州大学圣地亚哥分校数学教授 Ben Chow。公开资料显示，他于 1986 年在普林斯顿获得博士学位，导师是丘成桐。文中称，Hamilton 提出 Ricci 流后不久，丘成桐曾向他指出，这个流会在空间细的地方把它勒断，这可能正是证明的第一步，Hamilton 后来也回忆过这件事。
2025 年秋天，Ben Chow 与同行开设 Lean 线上学习班，从头学习这套工具。当时 Mathlib 连黎曼几何最基础的工具都还不完整。随后，Chow、Ziyang Qin 和 UCSD 博士生 Yuan Liao 用 7 个月先写出约 200 万行基础代码。
Ziyang Qin 是今年 5 月刚从康奈尔毕业的本科生，博士尚未开始。仓库中 11000 多次提交里，有 7477 次记在他的名下。9 月，来自普林斯顿的 Ayush Khaitan 带着拓扑工具加入，4 人一起完成了最后两周的冲刺。
文中披露，团队使用的 AI 主力包括 ChatGPT Astra 和 Claude Fable。按其开源工具包的结构，最上层是研究者直接对话的「领队」会话，本身不写证明，负责把住数学路线；其下有长期运行的「调度」智能体，负责拆分任务、分派任务和验收；真正执行写证明、找错和查资料的，是一批完成单项任务后退出的临时智能体。人类作者位于整套系统最上层，负责选择定义、设定命题，并确认 Lean 里证出的内容就是数学家要证明的命题。
9 月冲刺：先搭骨架，再逐步补全
冲刺阶段，团队正按照拓扑学家 Moise 于 1977 年出版的一本教材，逐节形式化拓扑部分。
9 月 20 日一早，Claude Fable 5.1 以「领队」身份写出一份任务单，把相关内容拆成 4 条并行任务线，交给 OpenAI 的编程智能体 Codex。每条任务线只能修改自己负责的文件，完成后提交清单，再由 Claude 验收并提交。
团队设定的一条原则是，绝不为了让命题可证而削弱命题；如果发现命题本身是假的，也算完成任务，给出反例后立即报告。
当天晚上，领队重新排出计划表。按 3 到 4 条任务线并行估算，教材中「公认最难」的几节需要 6 到 10 周，走到拓扑版庞加莱猜想最快也要 4 个多月。
半小时后，人类负责人决定改用另一种方式：先搭骨架。也就是先把整段证明结构写出来，暂时无法证明的步骤先用 sorry 占位，提前暴露接口不匹配的问题，再逐个审查、定稿并补证。这些骨架文件单独存放，不进入主库，因此最终成品里没有一个 sorry。
9 月 23 日，Ben Chow 一侧完成了第 32 节中的 3 个部分，由 Claude 领队验收。编译和审计都零报错后，这部分内容才被并入主库。第二天，教材从 25.2 到 34.1 的一串定理全部证完。美东时间 9 月 27 日凌晨 3 点 38 分，拓扑版庞加莱猜想完成，距离那张计划表排出还不到一周。
庞加莱猜想与「手术」方法
庞加莱猜想由庞加莱在 1904 年提出。其内容是：一个有限、封闭的三维空间，如果任意一根绳圈都能收缩成一个点，那么它就是三维球面。
这道题拖了近百年。更高维版本更早被解决，三维情形一直没有突破。直到 2002 年底到 2003 年，佩雷尔曼在 arXiv 连续发布 3 篇论文，用 Ricci 流完成证明。
Ricci 流的思路是把空间不断「熨平」。如果一个空间最终能被熨成处处一样圆，它就是球面。难点在于，空间演化过程中不一定平稳。文中用哑铃作比喻：两头是大球，中间连着一根细杆。Ricci 流运行后，细杆会越来越细，并在有限时间内被勒断，断裂点的曲率趋于无穷大，这就是奇点。
Hamilton 长期卡在这一步。佩雷尔曼借助典范邻域定理，知道快出问题的区域只能是「颈」或「帽」，于是引入「手术」：在细管即将断裂前，从颈部中间剪开，去掉即将出问题的一小段，再给两个断口各缝上一个标准帽子，让 Ricci 流继续运行。
23 行最终定理背后，是数百万行代码
佩雷尔曼在第三篇论文中还证明，对单连通空间来说，经过「流一段、做一次手术、再继续流」的过程，整个空间会在有限时间内缩到消失。消失的每一块都是三维球面，按剪开的位置粘回去后，得到的仍是三维球面。
这 3 篇论文中的许多关键步骤最初只给出结论。直到 2006 年，几组数学家分别写出数百页的详细版本，数学界才确认这套证明成立。
而在这次仓库中，前述约 402 万行代码，最终都服务于一个只有 23 行的文件。文件中的定理正是庞加莱猜想：任何紧致、单连通、无边界的三维拓扑流形，都与三维球面同胚。
由于 Ricci 流只能在光滑空间上运行，还需要 Moise 定理搭桥。Moise 在 1952 年证明，每个三维拓扑流形都可以被分解成小四面体拼接的形式，再把拼缝处理光滑，从而获得光滑结构。那 23 行代码的后半部分，就是先用 Moise 定理得到光滑结构，再调用光滑版庞加莱猜想。
文中称，Moise 这座桥比手术部分还更费代码。负责这部分的 PL 拓扑代码有 46 万行，比手术部分多出将近一倍。对于为何最后几行不能直接调用光滑版庞加莱猜想，Ayush Khaitan 回应称，参数 C 和 hC 不能省，因为 Lean 需要先确认该流形具备一套光滑坐标，而这两个参数正是从 Moise 定理中得到的。
从 2.5 万行到 470 万行
文中提到，一年前，自动形式化智能体 Gauss 用 3 周写出 2.5 万行代码，已经引发关注。这一次，4 名研究者加上一组 AI，在两周内写出的规模超过其 100 倍。
斯坦福数学家 Jared Duker Lichtman 在转发时连用了两个感叹号。按文中的描述，这支小队的分工已经接近未来数学研究的一种工作方式：资深研究者负责方向，年轻研究者带着 AI 一行行写代码，最终由 Lean 内核判断证明是否成立。人类数学家的工作重心，也在从逐步书写证明，转向判断该证明什么，以及识别 AI 写错的地方。
本文援引的参考资料包括 Ayush Khaitan 的 X 帖文、qinz1yang/differential-geometry 仓库及其 pull request、arXiv 论文、auto-formalizing-skills 仓库、Ben Chow 的 LeanOnMe 页面、Keith Adler 的 X 帖文，以及 math.inc 关于 Gauss 的页面。原文署名为微信公众号「新智元」（ID：AI_era），作者为「ASI启示录」。