IXThinker·2026-09-30 12:20

北大團隊完成龐加萊猜想Lean 4形式化

北京大學AI for Math團隊宣布，在Lean 4中完成千禧年難題龐加萊猜想的完整形式化，並同時通過兩套獨立檢驗。團隊藉智能體協作，約半個月、成本不足三萬美元即產出約三百二十萬行代碼。

世紀難題的形式化

龐加萊猜想由龐加萊於一九〇四年提出，二〇〇二年佩雷爾曼以不到七十頁的精簡預印本完成證明，其後數學界耗費數年撰寫逾五百頁專著。將其完整形式化，是形式數學領域的標誌性挑戰。