北大团队半月不到3万美元完成千禧难题庞加莱猜想Lean4形式化
近日，北京大学AI for Math团队宣布完成了千禧年大奖难题之一——庞加莱猜想在Lean 4中的完整形式化验证。这一成果不仅刷新了数学证明机器化的纪录，更标志着大规模智能形式化验证时代的正式到来。
庞加莱猜想于1904年被提出，2002年俄罗斯数学天才佩雷尔曼发布了不到70页的精简证明预印本。此后，数学界顶尖学者耗费数年时间，补全了证明中的所有细节，最终形成了一本500多页的权威专著。
而北大团队仅用半个月时间，就将这一复杂的数学证明转化为约320万行可被机器验证的代码，整体花费不到3万美元。据团队透露，这是目前已知首个同时通过Lean构建与官方Comparator检验的庞加莱猜想形式化版本。
完成这项工作的核心团队由3名具备数学背景的AI开发者牵头，搭配多位数学方向的博士后与博士生。他们借助公开商用大模型完成了海量的基础推导与代码编写，单行走线成本不到1美分。按照团队此前的估算，一位人类形式化专家每天约能完成250行代码，按每年250个工作日计算，320万行代码需要一位专家连续工作50年才能完成。此次项目的日均代码产出超过20万行，相当于800多名人类专家同时协作的效率。
值得注意的是，就在北大团队发布成果的当天，由丘成桐弟子带队的美国团队也完成了一份470万行的庞加莱猜想Lean证明，两支队伍均为独立完成，这一巧合进一步印证了大规模机器形式化验证时代的来临。
团队背景与前期成果
这支来自北京大学北京国际数学研究中心的团队对外以FrenzyMath为名，其核心目标是通过大模型与AI智能体加速现代数学研究进程。团队负责人为北大博雅特聘教授董彬，今年3月他们曾使用自研的Archon系统完成两道研究级数学题的形式化，其中一道题的AI生成代码约8800行，耗时50小时，花费1200美元，单行走线成本约0.14美元。到此次庞加莱猜想项目中，单行走线成本已降至当时的十几分之一。
今年4月，团队通过两个智能体接力协作——一个负责推导证明思路，另一个负责将其转化为Lean代码，仅用80小时就解决了交换代数领域D. D. Anderson在2014年提出的公开问题。同年8月，他们的AI智能体还帮助数学家推翻了拟阵Kazhdan–Lusztig多项式的两个重要猜想。同月，团队开源了Archon Horizon调度系统，用于指挥Codex或Claude Code等智能体长时间开展形式化工作，该系统当时正在推进的两个项目中就包括庞加莱猜想的形式化验证。
项目实施与难点突破
此次项目的核心并非直接复刻佩雷尔曼的证明，而是将Morgan与Tian刚的500页专著完整转化为Lean可验证的代码，团队的核心秘诀在于人类智慧与AI智能体的协同配合。3名核心开发者并未直接手写数百万行代码，而是负责设计、搭建并运行复杂的智能体工作流，多位数学背景的研究人员作为志愿者参与其中，指挥AI完成海量的基础推导与代码编写工作。
庞加莱猜想的证明深度依赖黎曼几何、微分几何、拓扑学以及偏微分方程等多个数学领域的理论基础，但当前的Lean 4官方数学库Mathlib中，这些领域的大量基础理论尚属空白。因此，北大团队不仅完成了证明本身的形式化，还在项目内部从头搭建了所有必要的前置理论体系。
项目于今年7月在GitHub正式建仓，团队首先编写了一份可供人类阅读的“蓝图”，该蓝图分为六章，列出了279条定义与定理，并清晰标注了每条内容在原专著中的出处。团队还将16份教科书、讲义与论文转化为配套的蓝图体系，覆盖从光滑流形、黎曼几何到偏微分方程的全部前置知识，其中两本参考的Ricci流教材作者还包括美国团队的带头人Ben Chow。8月中旬的审查记录显示，当时蓝图中仍有11个“外部接口”，即暂时借用外部结论的环节，但到9月28日交付的最终代码中，所有这些外部接口均已被验证或绕过，未使用任何sorry或额外公理。整个代码体系按照蓝图拆分为83个里程碑，从最基础的Ricci流理论推导一直延伸到最终的庞加莱猜想证明。根据对仓库的统计，整个项目包含27203个Lean文件，最终直接支撑庞加莱定理的核心代码约290万行，包含7.6万多条定理与引理。
代码细节与关键发现
从代码的具体分布来看，佩雷尔曼证明中最知名的手术操作部分对应约47万行代码，证明空间会在有限时间内收缩的部分约39万行代码。而整个项目中规模最大的单个里程碑是编号为M76的环节，单就这一部分就撰写了约65万行代码，规模是第二名的近三倍，其核心任务是在拓扑流形与光滑流形之间建立等价性转换——这是因为庞加莱猜想讨论的是拓扑空间，而Ricci流只能在光滑空间上运行，因此需要证明任何三维拓扑流形都可以被分解为可光滑化的小块。这一结论其实是上世纪五六十年代就已证明的经典定理，但在Lean中形式化时，对应的代码量甚至超过了佩雷尔曼手术部分的代码，美国团队在同一环节也撰写了约46万行代码。
此外，83个里程碑共用的公共库Horizon约有84万行代码，其中近四成是Ricci流的通用理论，另有十余万行黎曼几何代码与二十余万行拓扑代码，这些内容均为Mathlib中未收录的全新理论。即使是数学家默认的常识性结论，在机器形式化中也需要从头验证：比如平面上不自交的闭合曲线会将平面分为内部与外部的若尔当曲线定理，对应的代码就有3000多行；而进一步证明该曲线围成的内部同胚于圆盘的Schoenflies定理，相关代码更是达到了11.6万行。
将整本专著转化为机器代码的过程，也是一次全面的学术审查。北大团队在8月的审查文档中就发现了原专著中的一处错误：Morgan与Tian刚所著专著的附录A.19给出了一个无条件结论，称处处由“颈”（Ricci流中的细长圆管结构）组成的三维空间必然是一根直管。团队通过构造反例推翻了这一结论：将一根直管首尾相连形成的环面S²×S¹，虽然每一处看起来都符合颈的特征，但显然并非直管。最终团队弃用了A.19的结论，改用相邻的A.20条款，将结论修正为“要么是一根直管，要么是一个环面”。A.19所在的颈帽拓扑部分也是项目中第二大的里程碑，对应约22万行代码。
严格验证与行业意义
代码完成后，需要经过严格的验证流程。北大团队此次交付的版本是首个同时通过Lean原生构建与Lean官方Comparator工具检验的庞加莱猜想形式化版本。Comparator作为Lean官方的验证工具，会严格校验代码与原始证明的一致性，要求证明仅使用三条标准公理，并通过内核逐步验证每一步推导。为了进一步确保可靠性，团队还使用了独立开发的nanoda内核对整个证明进行了二次校验，这一验证方案与Anthropic此前完成费马大定理形式化时所使用的方案一致。
此次项目仅花费3万美元的成本，彻底改变了数学证明的验证方式。在传统模式下，一位数学家发布重大证明后，整个数学界需要花费数年时间逐页审读验证：佩雷尔曼的证明发布后，全球顶尖数学家团队耗时三四年才最终确认其正确性。而现在，将复杂证明转化为机器可验证的代码并完成全流程校验，仅需要半个月时间与一个实验室完全可以承担的预算。
一年多前，AI在奥数竞赛中取得金牌还属于突破性新闻，而如今，困扰数学界近百年的千禧年难题，仅需3万美元即可完成完整的形式化验证。不久前Anthropic宣布完成费马大定理的1300万行形式化验证，进一步印证了AI赋能的数学证明形式化即将迎来爆发式增长。
