北大团队 AI 智能体完成庞加莱猜想 Lean 4 形式化

北京大学 AI for Math 团队宣布，已在 Lean 4 中完成庞加莱猜想的完整形式化验证。庞加莱猜想是千禧年大奖难题之一，由庞加莱 1904 年提出，佩雷尔曼 2002 年以不到 70 页的预印本给出证明，学界此后又耗费数年撰写超 500 页专着才把论证补全。

这次的不同在做法：团队借助 **AI 智能体协作**推进，**约半个月、耗资不足 3 万美元**,把上述证明转化为约 320 万行形式化代码。报道把效率与成本称为新纪录。具体的技术路径、验证细节与可复现材料见原文（智源社区文章）。

💡 为什么值得看不到 3 万美元半月产出 320 万行代码，千禧年难题进机器可校验环境。