北大用 AI 把庞加莱猜想写进了 Lean：320 万行代码、3 万美元、半个月
北大北京国际数学研究中心的 FrenzyMath 团队，宣布独立完成了庞加莱猜想在 Lean 4 里的完整形式化。据团队说法，这是目前已知首个同时通过 Lean build 和 Comparator 检验的版本。
1904 年庞加莱提出这个猜想，2002 年佩雷尔曼给出不到 70 页的预印本，后来数学界花了好几年、写出 500 多页专著才把细节补齐。这次北大团队和 AI 智能体协作，半个月、不到 3 万美元，把它转成了约 320 万行代码。账是这么算的：北大团队此前给过估算，人类专家一天大约写 250 行，按一年 250 个工作日算，320 万行交给一个人得写整整 50 年。
不是靠手写，是当「包工头」
这支队伍对外叫 FrenzyMath，目标就是用大模型和 AI 智能体给现代数学研究提速。3 名有数学背景的 AI 开发者带着多位博士后、博士生，用公开的商用大模型做这件事。他们没有去手写几百万行代码，而是设计、搭建、运行一套复杂的智能体工作流——按材料里的说法，一行代码成本连 1 美分都不到。
这个成本是砍下来的。今年 3 月他们用自研的 Archon 系统形式化两道研究级数学题时，其中一道 AI 写了约 8800 行、跑了 50 个小时、花了 1200 美元，平均每行约 0.14 美元。到庞加莱猜想这里，每行成本降到了当时的十几分之一。这 3 万美元包括大模型调用费和计算服务器开销。
这也不是团队今年唯一一件战绩。4 月他们让两个智能体接力，一个想证明、一个写 Lean 代码，解决了交换代数里 D. D. Anderson 在 2014 年提出的一个公开问题，全程约 80 小时。8 月又帮数学家推翻了拟阵 Kazhdan–Lusztig 多项式的两个重要猜想。
最难的其实不是佩雷尔曼，是「地基」
佩雷尔曼证明的核心难点，工程里约 47 万行。证明空间会在有限时间缩没的那部分约 39 万行。但全仓最大的一块硬骨头是编号 M76 的里程碑，一个就约 65 万行，是第二名的将近 3 倍。
它的活是在「拓扑流形」和「光滑流形」之间修一座桥。庞加莱猜想说的是拓扑空间，Ricci 流却只能在光滑空间上跑，所以得先证明任何三维拓扑流形都能切成小四面体拼起来、再处理光滑。这是上世纪五六十年代就证完的老定理，一放进 Lean，写出来的代码比佩雷尔曼的手术还多，美国团队在同一处也写了 46 万行。
83 个里程碑共用的公共库 Horizon 约 84 万行，里面近四成是 Ricci 流通用理论，另有十多萬行黎曼几何、二十多万行拓扑——都是 Mathlib 里还没有、只能项目里自己搭的。数学家默认的常识在机器面前也得从头证：若尔当曲线定理一句大白话，写了 3000 多行；它延伸出的 Schoenflies 定理，代码 11.6 万行。
7 月项目在 GitHub 建仓，先写人能看懂的「蓝图」，分六章列出 279 条定义和定理，每条标明书里出处。团队还把 16 份教科书、讲义、论文都做成配套蓝图。到 9 月 28 日交付的代码里，没有一处 sorry，也没有一条额外公理。
挑出名著一处错，还过了双重检验
把书搬进 Lean，等于把每一句话重新审一遍。8 月审查文档里记着一处错误：Morgan 和田刚书中附录 A.19 的印刷版给了个不带条件的结论，大意是一个处处都由「颈」组成的三维空间一定是一根管子。但这有现成反例——把一根管子首尾粘成环，每一处看着还是颈，却不再是管子，这个环在三维里叫 S²×S¹。团队于是弃用 A.19，改用相邻的 A.20，结论改成「要么一根管子，要么一个环」。
检验这关，北大交的是首个同时通过 Lean 编译和 Comparator 检验的版本。Comparator 是 Lean 官方出的判卷工具，题目要和试卷一字不差，证明只准用三条标准公理，还要被内核逐步接受。北大还加了一道保险，请另一套独立写成的内核 nanoda 从头到尾再判一遍——Anthropic 前不久把费马大定理形式化成 1300 万行代码时，用的也是这一套。
3 万美元这个价格，改变的是数学界验证证明的方式。过去一个重大证明要好几组顶尖数学家审上三四年，现在一行行写成机器能懂的代码、再从头查到尾，只要半个月，加一个实验室付得起的预算。一年多前 AI 拿奥数金牌还算大新闻，今天一道困扰了数学界近一百年的千禧年难题，可以用这个量级的预算去验证。AI 赋能的数学证明形式化，接下来大概会很快爆发。