北大团队完成庞加莱猜想Lean 4完整形式化验证

北京大学AI for Math团队宣布独立完成庞加莱猜想在Lean 4中的完整形式化，将500多页专著转化为约320万行代码。该工作由开发者与学生借助商用大模型及智能体工作流协作完成，历时半个月、总花费不到3万美元，平均每行代码成本不足1美分。成果包含27203个Lean文件且无一处sorry标记，已同时通过Lean build与Comparator双重检验。