新智元报道
刚刚，北京大学 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
编辑：摩西 Aeneas
