北大团队完成庞加莱猜想 Lean 4 完整形式化，首个双检验版本

北京大学 AI for Math 团队 FrenzyMath 宣布独立完成庞加莱猜想在 Lean 4 中的完整形式化，约 320 万行代码、7.6 万多条定理与引理，是目前已知首个同时通过 Lean build 与 Comparator 检验的版本。项目由 3 位有数学背景的 AI 开发者带领多位博士后和博士生，与智能体协作半个月完成，花费不到 3 万美元，每行代码成本不到 1 美分。