北大团队官宣：庞加莱猜想被完整形式化！首个双检验版本来了

luyuanhong

北大团队官宣：庞加莱猜想被完整形式化！首个双检验版本来了

原创  ASI 启示录  新智元  2026 年 9 月 29 日 11:40  北京



刚刚，北京大学 AI for Math 团队宣布：他们独立完成了千禧年大奖难题之一 ——庞加莱猜想在 Lean 4 中的完整形式化！

1904 年，庞加莱提出猜想；2002 年，俄罗斯数学天才佩雷尔曼给出不到 70 页的精简证明预印本；随后，数学界顶尖大脑耗费数年，写出 500 多页的专著。

而今天，北大团队与智能体协作，仅用半个月时间，花费不到 3 万美元，就将其转化为约 320 万行代码！

据团队透露，这是目前已知首个同时通过 Lean build 与 Comparator 检验的庞加莱猜想形式化版本。



完成这项工作的，是 3 个有数学背景的 AI 开发者，带着多位博士后和博士生。他们用公开的商用大模型，一行代码成本连 1 美分都不到。

按北大团队此前给过的估算，人类专家埋头干一天，大约能写 250 行。一年按 250 个工作日算，这 320 万行交给一个人来写，得写整整 50 年。

就在北大团队发布成果的当天，丘成桐的弟子带队的美国团队，也交出了一份 470 万行的庞加莱猜想 Lean 证明。

两支队伍各自独立完成，却在同一天交卷。大规模机器形式化验证的时代，真的来了。

01  北大团队，半年成本降到十几分之一

这支队伍来自北京大学北京国际数学研究中心，对外叫 FrenzyMath ，目标是用大模型和 AI 智能体给现代数学研究提速。

团队今年 3 月和 4 月的两篇代表作，署名最后一位都是北大博雅特聘教授董彬。

今年 3 月，他们用自研的 Archon 系统，形式化了两道研究级数学题。

其中一道，AI 写了约 8800 行，跑了 50 个小时，花了 1200 美元，平均每行约 0.14 美元。

到了庞加莱猜想这里，每行代码的成本降到了当时的十几分之一。



速度也快得惊人。半个月写出 320 万行，平均每天 20 多万行，相当于 800 多个人类形式化专家同时开工。

这 3 万美元，包括大模型的调用费和计算服务器的开销。



这支团队今年的战绩不止这一件。

4 月，他们让两个智能体接力，一个负责想证明，一个负责写成 Lean 代码，解决了交换代数里 D. D. Anderson 在 2014 年提出的一个公开问题，全程约 80 个小时。

8 月，他们的智能体又帮数学家推翻了拟阵 Kazhdan–Lusztig 多项式的两个重要猜想。

同样在8月，团队开源了一套叫 Archon Horizon 的调度系统，专门指挥一群 Codex 或 Claude Code 智能体长时间做形式化。它当时列出的两个在跑项目，其中一个就是庞加莱猜想。



02  照着 500 页专著，拆成 83 个里程碑

佩雷尔曼当年的三篇预印本，加起来不到 70 页，很多关键步骤只写了结论。后来 Morgan 和田刚为了把细节补齐，写出了一本 500 多页的专著。

北大的目标，就是把这本书整个搬进 Lean 。

他们的核心秘诀，就是「人类智慧 + AI 智能体」的完美协同。

在这个项目中，3 具有数学背景的 AI 开发者成为了「包工头」。

他们没有自己去手写数百万行代码，而是设计、搭建并运行了复杂的智能体工作流。

多位数学方向的博士后、博士生作为志愿者加入，他们运用公开的商用大语言模型，指挥 AI 去完成海量的基础推导和代码编写。

这其中的最大难点，其实不在于庞加莱猜想本身，而在于「地基」。

庞加莱猜想的证明，深深扎根于黎曼几何、微分几何的土壤，同时还需要调用拓扑学、偏微分方程等极其广泛的数学工具。

然而，在当前的 Lean 4 库（Mathlib）中，这些高深领域的大量基础理论完全是一片空白。

好在，北大团队在半个月内，不仅完成了塔尖的建设，还在项目内部从头搭建了所有这些前置理论的庞大地基。

7 月，项目在 GitHub 上建仓，先写了一份人能看懂的「蓝图」。蓝图分六章，列出 279 条定义和定理，每一条都标明在书里的出处，谁引用谁画得清清楚楚。

打地基也是同样的做法。

团队把 16 份教科书、讲义和论文都做成了配套蓝图，从光滑流形、黎曼几何，一直到偏微分方程。其中两本用作参考的 Ricci 流教材，作者里都有美国团队的带头人 Ben Chow 。

8 月中旬审查时，蓝图里还挂着 11 个「外部接口」，也就是「这一步先借用别人的结论」的白条。

到了 9 月 28 日交付的代码里，没有一处 sorry ，也没有一条额外公理。这 11 张白条，要么在 Lean 里被证了出来，要么被绕开了。

真正的代码，按蓝图拆成了 83 个里程碑，从最底层的 Ricci 流基础估计，一路推到最后的总装。



我们把北大的仓库完整下载下来做了统计，一共有 27203 个 Lean 文件。

最终那两条庞加莱定理层层引用到的代码约 290 万行，里面有 7.6 万多条定理和引理。





03  最贵的一块，竟然不是佩雷尔曼

佩雷尔曼最出名的手术，在这个工程里写了约 47 万行。证明空间会在有限时间里缩没的那部分，约 39 万行。

全仓最大的一块硬骨头，却是编号 M76 的里程碑。它一个就写了约 65 万行，是第二名的将近 3 倍。

它干的活，是在「拓扑流形」和「光滑流形」之间修一座桥。

庞加莱猜想说的是拓扑空间，Ricci 流却只能在光滑的空间上跑。所以必须先证明，任何三维拓扑流形都能切成一块块小四面体拼起来，再把缝隙处理光滑。



这是上世纪五六十年代就证完的老定理，一放进 Lean ，写出来的代码却比佩雷尔曼的手术还多。美国团队在同一处也写了 46 万行。

另一大块，是 83 个里程碑共用的公共库 Horizon ，约 84 万行。

里面近四成是 Ricci 流的通用理论，另有十多万行黎曼几何、二十多万行拓扑，都是 Mathlib 数学库里还没有、只能在项目里自己搭的东西。



连数学家心里默认的常识，在机器面前也得从头证一遍。

平面上画一个不自交的圈，里面和外面就被分开了，这是若尔当曲线定理。就这么一句大白话，库里写了 3000 多行。

再进一步，这个圈围出来的里面恰好是一块圆盘，这是 Schoenflies 定理，相关代码写了 11.6 万行。

04  挑出名著一处错，还过了双重检验

把一本书搬进 Lean ，就是把书里的每一句话拿出来重新审一遍。

北大项目 8 月的一份审查文档里，就记着这样一处错误。

Morgan 和田刚书中附录 A.19 的印刷版，给了一个不带任何条件的结论，大意是一个处处都由「颈」组成的三维空间，一定是一根管子。（「颈」指的是 Ricci 流里那种细长的圆管。）

而审查文档一句话就把它推翻了。

把一根管子首尾相连粘成一个环，每一处看着都还是颈，可它显然不再是一根管子。这个环在三维里叫 S^2×S^1 ，正是书里结论的现成反例。

于是团队弃用了 A.19 ，改用书里相邻的 A.20 ，结论变成「要么是一根管子，要么是一个环」。A.19 所在的颈、帽拓扑那一段，是全仓第二大的里程碑，写了 22 万行。



代码写完，还得过考官这一关。

据悉，北大这次交出的，是首个同时通过 Lean 编译和 Comparator 检验的版本。

Comparator 是 Lean 官方推出的判卷工具，像一位铁面无私的考官。答卷的题目必须和试卷一字不差，证明只准用三条标准公理，还要被内核逐步接受。

不仅如此，北大还多加了一道保险，请另一套独立写成的内核 nanoda ，把这份证明从头到尾再判一遍。





Anthropic 前不久把费马大定理形式化成 1300 万行代码时，用的也是这一套。

05  千禧年难题的验证，只要 3 万美元

3 万美元这个价格，改变的是数学界验证证明的方式。

过去，一位数学家拿出一个重大证明，整个数学界得花上好几年一页页审读。佩雷尔曼的证明贴出来之后，好几组顶尖数学家花了三四年，才确认它站得住。

现在，把它一行行写成机器能懂的代码，再从头查到尾，只要半个月，外加一个实验室付得起的预算。

一年多前，AI 拿下奥数金牌还是大新闻。今天，一道困扰了数学界将近一百年的千禧年难题，可以用 3 美元去验证。

就在不久前，Anthropic 也宣布完成了费马大定理的形式化验证。

无数事实证明：AI 赋能的数学证明形式化，将很快大爆发。

参考资料：

https://frenzymath.com/news/poincare-formalization
https://github.com/frenzymath/PoincareConjecture
https://github.com/frenzymath/Poincare-Conjecture
https://github.com/LehengChen/PoincareConjecture
https://frenzymath.com/news/archon-firstproof/
https://frenzymath.com/blog/conjecture/
https://www.thepaper.cn/newsDetail_forward_33693886
https://frenzymath.com/blog/archon-horizon/
https://github.com/leanprover/comparator
https://github.com/anthropics/fermats-last-theorem
https://github.com/qinz1yang/differential-geometry

编辑：摩西 Aeneas

新智元

重生888@

北大团队，一行代码0.14美元，大约·是一元人民币，8800元费用是私人出，还是公家出？