北大团队半月完成庞加莱猜想形式化，成本不到3万美元

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

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

完成这项工作的，是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万美元包括大模型调用费和计算服务器开销。团队今年战绩不止这一件。