AI首度驗證素數研究最前沿定理 形式化證明劍指AI程式碼安全

Axiom Math用自家AI系統AxiomProver，自動驗證了「246定理」的證明——這是素數研究目前所知的極限。創辦數學家Ken Ono說得直白：這個定理就是人類對素數認知的邊界。所謂246定理，講的是孿生質數猜想的逼近戰果：2013年張益唐證出無窮多對相差7000萬的質數，幾個月後Maynard把差距砍到600，再由Maynard與陶哲軒領軍的Polymath8b團隊壓到246——這是目前離「差距為2」的終極目標最近的一步，而AxiomProver把整條證明鏈的機器可讀版本從頭驗到尾。

形式化驗證不是萬無一失的橡皮圖章，近期就有案例顯示驗證方法本身的漏洞，能被用來放行一個實則錯誤的AI生成證明。但比起純靠人眼審查，這已經是最接近「蓋章保證」的做法。跟今年稍早Math, Inc.用Gauss agent形式化Viazovska球堆積問題證明相比，Axiom Math這次做的不是一次性任務——他們刻意把驗證過程拆成可重複使用的元件，建了一個關於質數間隙的結果庫，246定理只是這個庫裡的旗艦成果。這意味著下一個關於質數間隙的證明，不用再從零開始搭驗證框架。

真正的重點不在數論本身，而在Ono講的那句話：世界即將運行在沒有人讀過的程式碼上。他把這次證明形式化，看成驗證AI生成程式碼的一塊試驗田——如果一段程式碼「會不會終止」「輸出對不對」這些性質，能翻譯成精確的數學陳述，AxiomProver這類技術就有辦法拿去正式證明它。換句話說，AI寫的程式碼能不能安全上線，以後可能要靠另一套AI去做數學級的驗證，而不是靠人工code review。

這對商業決策者的意義很直接：AI生成程式碼已經在滲透基礎設施、金融系統、資料安全這些高風險領域，而幻覺與漏洞的風險始終存在。形式化驗證如果能從純數學圈，跨進軟體工程的日常流程，會是繼AI寫程式之後的下一個關鍵基礎設施——誰先把這套驗證能力產品化，誰就掌握了「AI程式碼能不能被信任」這個問題的答案權。素數研究本身冷門，但它撐起的是所有現代密碼學與資安系統的底層數學，這條線一旦打通，受益的不只是數學家。