Axiom Math 團隊宣佈，他們使用自主研發的 AI 系統 AxiomProver，首次自動驗證了數論中著名的“246 定理”的證明。該定理指出，存在無窮多對相差 246 的素數。這一成果被視為 AI 輔助數學研究的一個重要里程碑，標誌著 AI 在形式化驗證領域邁出了關鍵一步。
形式化驗證是一種讓計算機檢查機器可讀版本證明的方法。雖然這一過程並非 100% 保證證明正確——正如近期一項演示所揭示的，方法中的缺陷可能被利用來接受錯誤的 AI 生成證明——但計算驗證仍被數學家視為最接近“橡皮圖章”式的確認方式。Axiom Math 表示，此次驗證不僅形式化了一個重要的數論進展，更展示了未來如何利用自動化 AI 驗證來確保 AI 生成的計算機程式碼的正確性，這些程式碼即將支撐全球的軟體系統。
這並非 AxiomProver 的首次成功。Axiom Math 已使用其自主多智慧體系統，將數學陳述轉化為機器可檢查的證明，今年已攻克多個未解數學問題並驗證了更多證明。但 246 定理的形式化是迄今最具意義的成果。Axiom Math 創始數學家 Ken Ono 表示：“這個定理目前代表了人類對素數認知的閾值。”
此前，Axiom Math 的競爭對手 Math, Inc. 曾使用其 Gauss 代理，形式化了 Maryna Viazovska 2022 年菲爾茲獎獲獎證明——8 維和 24 維球體堆積問題。卡內基梅隆大學博士生 Sidharth Hariharan 曾領導人類團隊制定 Viazovska 證明的形式化藍圖，他認為 246 定理的形式化是更全面、更有用的成就。Hariharan 現為 Axiom Math 實習生，深度參與了 246 定理證明的形式化工作。他指出，與一次性處理單一問題不同，Axiom Math 明確致力於使形式化的元件可重複用於其他形式化任務和數學研究。團隊利用 AxiomProver 構建了一個關於素數間隙的結果庫，246 定理是該庫中的旗艦成果。
“246 定理”源於孿生素數猜想。該猜想由法國數學家阿爾方斯·德·波利尼亞克在 19 世紀首次精確表述，認為存在無窮多對相差 2 的素數（孿生素數）。儘管表述簡單，但該猜想至今未被證明。2013 年，張益唐（現為廣州中山大學教授）證明了存在無窮多對相差 7000 萬的素數，首次取得突破。幾個月後，牛津大學教授 James Maynard 用不同技術將這一差距從 7000 萬大幅縮小到 600，這一成就為他贏得 2022 年菲爾茲獎做出了重要貢獻。作為 Polymath8b 合作組織成員，Maynard 和菲爾茲獎得主、加州大學洛杉磯分校教授 Terence Tao 將差距進一步縮小到 246，這是數學家們最接近目標差距 2 的一次。AxiomProver 驗證的正是這個“246 定理”——存在無窮多對相差 246 的素數。
這項工作的意義不僅限於數論。數論是現代密碼學和網路安全的基礎，因此形式化驗證可能有助於未來驗證我們保護數字資料的具體方式。但 Ken Ono 更看重更宏大的圖景：他將形式化數學證明視為驗證 AI 生成程式碼的墊腳石。隨著 AI 生成的程式碼開始應用於社會各個領域，如基礎設施執行、金融管理和資料保護，其安全性備受關注。如果程式碼的屬性（如演算法是否終止、程式輸出對任何輸入是否正確）能被轉化為精確的數學陳述，那麼源自 AxiomProver 的技術將非常適合正式陳述並證明這些屬性。這樣一來，數學上驗證 AI 生成程式碼的正確性將使這些程式碼可以安全使用。Ono 總結道：“世界即將執行在沒人讀過的計算機程式碼上。AI 已經到來，我們不能再視而不見——證明形式化是解決我認為我們將面臨的最重要挑戰的試驗場。”