IXThinker·2026-09-29 12:50

AI助攻470萬行代碼 千禧難題證明首獲完整驗證

千禧難題龐加萊猜想完整證明首次被寫成機器可驗證代碼：四人團隊以證明助手逐行形式化，總計約470萬行並全數通過內核檢查，其中約270萬行在最後兩周由人工智能協力完成，為機器驗證複雜定理立下里程碑。

四人小隊加AI

團隊帶頭人是研究微分幾何數十年的資深學者，亦是知名數學家的弟子，衝在最前的是一名應屆畢業本科生，背後是一群全天候待命的人工智能。如此組合把一項曠日持久的大工程壓縮到數月內完成。