庞加莱猜想的同日双卷：320万行与470万行，一次三万美元的验证

1904 年庞加莱写下那个猜想。2002 年佩雷尔曼贴出三篇预印本，加起来不到 70 页。此后一批顶尖数学家花了三四年逐页核对，又写出 500 多页的专著，把他跳过的步骤补齐。

2026 年 9 月 29 日，两支互不相识的队伍在同一天宣布，这条路线已经被完整写进了 Lean。

一支在北京大学北京国际数学研究中心，对外叫 FrenzyMath。另一支由加州大学圣地亚哥分校的 Bennett Chow 领衔，论文挂在 arXiv:2609.33842，提交日期 9 月 27 日，署名是 Ziyang Qin、Yuan Liao、Ayush Khaitan、Bennett Chow。

📐 六分之一是佩雷尔曼，六分之五是论文里省略的地基

先看量级。美国团队整个仓库约 470 万行，全部通过 Lean 内核检查，没有一处用 sorry 留白。沿着最终那条庞加莱定理往回追引用，真正用到的代码是 14197 个文件、约 402 万行，最长的一条引用链串起 353 个文件。

佩雷尔曼三篇论文对应的代码约 66 万行，只占六分之一。第三篇只有 7 页，平均每页对应 1.4 万行；里面一句话带过的曲线缩短流，落进 Lean 就写了 7.6 万行。

剩下六分之五，是论文默认读者已经掌握的基础。分析学约 109 万行，微分几何约 77 万行，Moise 光滑化那座从拓扑流形通往光滑流形的桥 46 万行。最重的一块是典范邻域定理，撑起 272 万行，占整条依赖链三分之二；光是 DeTurck 技巧（把换坐标后变形的 Ricci 流方程改造成标准热方程）一项，就要用到 89 万行。

北大这边同样算得清楚。仓库共 27203 个 Lean 文件，最终两条庞加莱定理层层引用到的代码约 290 万行，里面有 7.6 万多条定理和引理。代码按蓝图拆成 83 个里程碑，最大的一块是编号 M76，单独写了约 65 万行，干的正是美国团队那 46 万行的活。佩雷尔曼最出名的手术写了约 47 万行，有限时间灭绝那一段约 39 万行。83 个里程碑共用的公共库 Horizon 约 84 万行，其中近四成是 Ricci 流通用理论。

两支队伍在完全独立的前提下，撞出了同一处最贵的地方。

🔍 让一本书过机器，A.19 那一条没过去

把专著搬进 Lean，等于把书里每一句话重新审一遍。北大项目 8 月的一份审查文档里记着这么一处：Morgan 与田刚那本书的附录 A.19，印刷版给了一个不带附加条件的结论，大意是一个处处都由「颈」组成的三维空间一定是一根管子。

审查文档用一句话推翻了它。把一根管子首尾相连粘成一个环，每一处看着仍然是颈，可它已经不是管子了。这个环就是 S²×S¹。团队因此弃用 A.19，改用相邻的 A.20，结论改成「要么是一根管子，要么是一个环」。

连数学家心里默认的常识，机器面前也得从头证。平面上画一个不自交的圈，里外就被分开，这是若尔当曲线定理，库里写了 3000 多行。再进一步，这个圈围住的里面恰好是一块圆盘，这是 Schoenflies 定理，相关代码 11.6 万行。

💰 三万美元，和每行不到一美分

北大的账是这么算的：半个月，不到 3 万美元，含大模型调用费和服务器开销，一行代码的成本不到 1 美分。今年 3 月他们用自研的 Archon 系统形式化一道研究级数学题，写了约 8800 行，跑了 50 小时，花了 1200 美元，平均每行约 0.14 美元。半年下来，每行成本降到了当时的十几分之一。

按团队此前给过的估算，人类专家一天大约写 250 行，一年按 250 个工作日算，320 万行交给一个人写要 50 年。半个月完成，相当于 800 多名人类形式化专家同时开工。

做这件事的核心是 3 位有数学背景的 AI 开发者带着多位博士后和博士生。他们不手写代码，而是搭智能体工作流：先写一份人能看懂的蓝图，分六章列出 279 条定义和定理，每条标明在书里的出处；再把 16 份教科书、讲义和论文做成配套蓝图。8 月中旬审查时蓝图里还挂着 11 张「这一步先借用别人结论」的白条，到 9 月 28 日交付的代码里，没有一处 sorry，也没有一条额外公理。

🧪 谁在签字

代码写完还得过考官。北大交出的是首个同时通过 Lean 编译与 Comparator 检验的版本。Comparator 是 Lean 官方的判卷工具，题目要求必须与试卷一字不差，证明只准用三条标准公理，还要被内核逐步接受。他们另外请了独立实现的另一套内核 nanoda，把整份证明从头再判一遍。Anthropic 此前把费马大定理形式化成 1300 万行时，用的也是这套双内核做法。

这里有个容易滑过去的地方要分清楚。形式化证明能保证的是这串形式推导没有漏洞，而「形式化是否忠实于佩雷尔曼的原证明」这一层，靠的是蓝图、人工审查和引用链追溯。北大能在书里挑出 A.19 的错，恰恰说明这一层是真在做事，而不是走过场。【判断】

⚖️ 该看什么，不该看什么

不该看的一点是「AI 独立证明了庞加莱猜想」。两支队伍做的都是把人类已有的证明搬进机器，没有产生新数学。

该看的是价格曲线。验证一个千禧年难题，过去要整个数学界顶尖大脑三四年；现在半个月加三万美元，一个实验室付得起。【推论】Tao 此前把这种转变描述为从证明稀缺走向证明丰裕，庞加莱猜想这一轮的规模与成本，把这个说法落到了具体数字上。

同时也该看到地基的代价。两支队伍各自重写了分析学与微分几何的大片基础，因为 Mathlib 里没有。这部分代码能不能回流进公共库，决定了下一个难题的形式化成本是继续按十几分之一的斜率下降，还是各自重复一遍。【判断】

同一天，还有两条更小的线在动：Lech Mazur 宣布基于 Codex 的智能体给出了 Collatz 猜想的新下界，对足够大的 X 至少有 cX 个正整数 n 小于 X 能在 10.46 ln(n) 步内回到 1，比例不为零，此前最好下界是 X 的 0.84 次方与 0.90 次方，并已完成 Lean 形式化；Vals AI 称 10 个 Claude Sonnet 5.5 智能体用约 15 小时生成了 Thomson 问题 N=7 的 17895 行 Lean 证明，结论是七个电荷的最低能量排布为五角双锥。

• 信源：新智元对北大团队的报道（9 月 29 日）、虎嗅对 UCSD 团队的报道、arXiv:2609.33842（9 月 27 日提交）、AGI Hunt 9 月 29 日日报
• 限定：Collatz 与 Thomson 两条目前只有团队自述与二手转述，未见同行评议，本文只作线索列出