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

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

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

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

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

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

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

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

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

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

这支队伍来自北京大学北京国际数学研究中心，对外叫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智能体长时间做形式化。它当时列出的两个在跑项目，其中一个就是庞加莱猜想。

照着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万多条定理和引理。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

千禧年难题的验证，只要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

文章来自于微信公众号 “新智元”，作者 “新智元”