北大团队官宣：庞加莱猜想被完整形式化！首个双检验版本来了

北京大学AI for Math团队宣布，他们独立完成了千禧年大奖难题之一——庞加莱猜想在Lean 4中的完整形式化。这是目前已知首个同时通过Lean build与Comparator检验的版本。

1904年庞加莱提出猜想，2002年佩雷尔曼给出证明预印本。数学界后续耗费数年写出500多页专著。北大团队与智能体协作，仅用半个月时间，花费不到3万美元，将其转化为约320万行代码。

这项工作由3名有数学背景的AI开发者主导，带领博士后和博士生使用商用大模型完成。按估算，人类专家需50年才能完成同等工作量。两支队伍独立完成，却在同一天交卷，标志着大规模机器形式化验证时代开启。

团队来自北京大学北京国际数学研究中心，目标是用大模型加速数学研究。今年3月他们用自研Archon系统形式化两道数学题，其中AI写了约8800行，成本约0.14美元/行。庞加莱猜想代码成本降至十几分之一，速度相当于800多人同时开工。

项目拆解佩雷尔曼的500页专著为83个里程碑，从最底层的Ricci流基础估计到最终总装。团队在GitHub建仓，先写「蓝图」分六章，列出279条定义和定理，每条标明出处。项目内部搭建了所有前置理论的地基。

代码总量达27203个Lean文件，约290万行，含7.6万条定理和引理。最贵部分并非佩雷尔曼证明，而是M76里程碑写了约65万行，用于连接拓扑流形与光滑流形。公共库Horizon约84万行，包含Ricci流通用理论和黎曼几何、拓扑等内容。

团队发现Morgan和田刚书中附录A.19的结论错误，改用A.20。代码需通过Lean编译和Comparator双重检验。Anthropic用类似方式完成费马大定理形式化。3万美元成本可验证千禧年难题，改变数学界验证方式。