刚刚，北京大学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
文章来自于微信公众号 “新智元”，作者 “新智元”