北大团队完成庞加莱猜想在Lean 4中的完整形式化

1. 11:24
   AITNT · AI头条精选

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

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

当前热度 6·可比范围峰值 10（9月30日 12:00）·近 24 小时可比范围变化 –

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。