庞加莱猜想提出来一百多年。
千禧年难题里，它是最早被攻克的那一个。
现在，北京大学一支团队宣布，他们把它跑通了。
用的工具是一个开源证明助手。
这个助手叫 Lean 4。
数学界这几年最认真对待的就是它。
牵头的是三位年轻开发者。
他们都有数学背景。
后面还跟着博士后和博士生志愿者。
这些人都是自愿来的。
他们调用的都是公开可调的商用大模型。
也就是普通人能在 AI对话 产品里调到的那一类。
这套打法说出来很朴素。
把它当成一件趁手的 AI工具 来使。
一行代码的成本，连一美分都不到。
按团队此前的估算，人类专家埋头干一天，大约能写 250 行。
一年按 250 个工作日算。
把这 320 万行交给一个人写。
得写整整 50 年。
2002 年，佩雷尔曼只交出三篇预印本。
三篇加起来不到 70 页。
后来为了让每个细节都站得住，两位数学家又补出一本专著。
那本书 500 多页。
而这一次，整个工程只花了半个月。
一、成本半年降到十几分之一
这支队伍挂在北京大学北京国际数学研究中心下面。
目标很直接。
用大模型和智能体，给现代数学提速。
今年 3 月，他们用自研系统形式化了两道研究级题目。
有一道写了约 8800 行。
跑了 50 个小时。
花了 1200 美元。
平均每行 0.14 美元。
到了庞加莱猜想这里，每行的成本降到了十几分之一。
速度同样惊人。
半个月写出 320 万行。
平均每天 20 多万行。
这个速度，相当于 800 多个熟练专家同时开工。
那 3 万美元里，装着模型调用费和服务器开销。
这支团队今年的战绩不止这一件。
4 月，他们让两个智能体接力。
一个负责想证明。
一个负责写成代码。
那一轮的题目是交换代数里的一个公开问题。
问题 2014 年提出。
全程约 80 个小时。
8 月，他们的智能体又推翻了两个重要猜想。
同样在 8 月，团队开源了一套调度系统。
它的活是指挥一群编程助手，长时间做形式化。
当时列出的在跑项目里，就有庞加莱猜想。
二、照着 500 页专著，拆成 83 个里程碑
目标说起来很简单。
把那本 500 多页的专著，整个搬进 Lean 库。
做法是人和智能体搭班子。
开发者更像包工头。
他们没有选择逐行手写。
而是把力气花在设计流程和调度上。
博士后和博士生志愿者负责指挥。
海量的基础推导和代码编写，都交了出去。
这本质上是一次规模空前的 AI编程 任务。
最难的地方不是猜想本身。
是地基。
庞加莱猜想的证明扎根在黎曼几何和微分几何里。
还要动用拓扑学、偏微分方程这些工具。
而在那个 Lean 库里，这些高深领域的基础理论几乎一片空白。
半个月里，团队不光建成了塔尖。
他们还顺手搭出了整片地基。
7 月，项目在开源仓库里建了仓。
先写了一份人能看懂的蓝图。
蓝图分六章，列出 279 条定义和定理。
每条都标着在书里的出处。
地基也是同样的做法。
团队把 16 份教科书、讲义和论文做成了配套蓝图。
8 月中旬审查时，蓝图里还挂着 11 个外部接口。
所谓外部接口，就是先借别人的结论打个白条。
到 9 月 28 日交付的代码里，没有一处占位符，也没有一条额外公理。
这 11 张白条，要么被证了出来，要么被绕开了。
真正的代码按蓝图拆成了 83 个里程碑。
从最底层的里奇流基础估计，一路推到总装。
把仓库整个下载下来做一次统计，一共 27203 个文件。
两条终点定理层层引用到的代码约 290 万行。
里面有 7.6 万多条定理和引理。
这两条定理，才是真正的交付物。
三、最贵的一块，不是佩雷尔曼的手术
佩雷尔曼最出名的那一步手术，写了约 47 万行。
证明空间会在有限时间里缩没的那部分，约 39 万行。
全仓最大的一块，是编号 M76 的里程碑。
它一个就写了约 65 万行。
接近第二名的三倍。
它干的活，是在两种流形之间修一座桥。
一头是拓扑流形。
另一头是光滑流形。
庞加莱猜想说的是拓扑空间。
里奇流却只能在光滑的空间上跑。
所以得先证明，任何三维拓扑流形都能切成小四面体拼起来。
再把缝隙磨平。
这是上世纪五六十年代就证完的老定理。
搬进 Lean 之后，代码量反而超过了佩雷尔曼的手术。
美国团队在同一处也写了 46 万行。
另一大块，是 83 个里程碑共用的公共库。
这一块约 84 万行。
里面近四成是里奇流的通用理论。
另有十多万行黎曼几何。
还有二十多万行拓扑。
这些内容在标准数学库里都没有。
只能在项目里自己搭。
连数学家心里默认的常识，在机器面前也得从头证一遍。
平面上画一个不自交的圈，里面和外面就被分开了。
这是若尔当曲线定理。
就这么一句大白话，库里写了 3000 多行。
再进一步，这个圈围出来的里面恰好是一块圆盘。
这是舍恩弗利斯定理。
代码写了 11.6 万行。
四、挑出名著一处错，还过了双重检验
把一本书搬进 Lean，等于把每句话拿出来重审一遍。
8 月的一份审查记录里，就记着这样一处错误。
那本专著的附录 A.19 给了一个不带条件的结论。
大意是处处由颈组成的三维空间，一定是一根管子。
颈指的是里奇流里那种细长的圆管。
审查记录一句话就把它推翻了。
把一根管子首尾相连粘成环，每一处看着都还是颈。
可它显然不再是一根管子。
这个环正是那条结论的现成反例。
团队没有硬扛 A.19。
他们换用了书里相邻的 A.20。
结论变成要么是一根管子，要么是一个环。
A.19 所在的那一段，是全仓第二大的里程碑。
一共写了 22 万行。
代码写完，还得过考官这一关。
按团队的说法，这个版本第一个同时通过了编译和判卷检验。
那位考官的要求很硬。
题目必须和试卷一字不差。
证明只准用三条标准公理。
还要被内核逐步接受。
团队还多加了一道保险。
他们请另一套独立写成的内核，把证明从头到尾再判一遍。
另一家美国公司前不久把费马大定理形式化成 1300 万行代码。
用的也是这一套。
3 万美元这个价格，改变的是数学界验证证明的方式。
过去一位数学家拿出重大证明，整个数学界得花好几年一页页审读。
佩雷尔曼的证明贴出来之后，好几组顶尖数学家花了三四年才确认它站得住。
现在把它写成机器能懂的代码，再从头查到尾，只要半个月。
外加一个实验室付得起的预算。
一年多前，模型拿下奥数金牌还是大新闻。
今天，一道困扰数学界近百年的难题，半个月就能验完。
真正被改写的是那道门槛。
