Axiom Math 團隊首次使用其 AI 系統 AxiomProver，自動驗證了與質數相關的「246 定理」證明。這項成就代表了 AI 輔助數學研究的一個重要里程碑。
在形式化驗證中，數學家會讓電腦檢查證明的機器可讀版本。儘管最近的演示顯示，這種方法可能存在漏洞，導致接受錯誤的 AI 生成證明，但計算方法仍是目前最接近「蓋章認證」的方式。這次特定的驗證，形式化了數論上的一項重要進展。
除了這個證明之外，它還展示了未來如何利用自動化 AI 驗證，來確保即將在全球軟體中使用的 AI 生成電腦程式碼的正確性。AxiomProver 並非首次亮相，Axiom Math 已經利用其自主多代理系統，將數學陳述轉化為機器可檢查的證明，解決了多個未解的數學問題，並在今年驗證了更多證明。
然而，Axiom Math 創始數學家 Ken Ono 解釋，246 定理的證明形式化是迄今為止最重要的成就，因為「這個定理目前代表了人類對質數知識的門檻」。今年稍早，Axiom Math 的競爭對手 Math, Inc. 曾使用其 Gauss 代理，形式化了 Maryna Viazovska 於 2022 年獲得菲爾茲獎的 8 維和 24 維球體堆積問題證明。
卡內基美隆大學博士生 Sidharth Hariharan 曾主導 Viazovska 證明形式化藍圖的人工工作，他認為 246 定理的形式化是一項更全面且更有用的成就。Hariharan 現在是 Axiom Math 的實習生，他深度參與了該公司 246 定理證明的形式化工作。
Hariharan 表示，主要區別之一在於，Axiom Math 並非針對單一問題採取一次性方法，而是明確旨在使形式化的組件可重複用於其他形式化任務和數學研究。該團隊已利用 AxiomProver 建立了一個關於質數間隙的結果庫，而 246 定理正是該庫中的旗艦成果。
那麼，什麼是 246 定理呢？最初的幾個質數彼此接近：2、3、5、7、11、13、17、19、23、29、31 等。其中有幾對質數的差為 2：3:5、5:7、11:13、17:19 等，這些質數對被稱為孿生質數。
孿生質數離零越遠越稀有，但它們似乎仍會偶爾出現。19 世紀法國數學家 Alphonse de Polignac 首次精確提出的孿生質數猜想認為，無論在數線上多遠，它們都會不斷出現，換句話說，存在無限多對孿生質數。
儘管易於陳述，但這個古老的孿生質數猜想至今仍未被證明。直到 2013 年，現任廣州中山大學教授張益唐證明存在無限多對相差 7000 萬的質數，才首次取得進展。幾個月後，牛津大學教授 James Maynard 採用不同技術，將這個間隙從 7000 萬大幅縮小到僅 600；這項壯舉為 Maynard 贏得了 2022 年菲爾茲獎（被廣泛認為是數學界的諾貝爾獎）。
作為 Polymath8b 合作小組的一員，Maynard 和另一位菲爾茲獎得主、加州大學洛杉磯分校教授 Terence Tao，將間隙縮小到僅 246；這是數學家們最接近目標間隙 2 的距離。正是這個「246 定理」，它指出存在無限多對相差 246 的質數，AxiomProver 已驗證其正確性。
這項工作中形式化的技術在數論中非常重要，數論是支撐所有當今網路安全和密碼學的數學分支。因此，它們可能在未來驗證我們保護數位資料的特定方式方面發揮作用。但 Axiom Math 的 Ono 對更大的前景更感興奮。
他將數學證明形式化視為驗證 AI 生成程式碼的墊腳石，這些程式碼正開始被社會廣泛應用於運行基礎設施、管理財務和保護資料的系統中。儘管人們對幻覺、錯誤和其他意外漏洞存在安全擔憂，但這項工作仍具重要意義。
如果程式碼的屬性，例如演算法是否終止，或者程式對於任何輸入的輸出是否正確，可以轉化為精確的數學陳述，那麼源自 AxiomProver 的技術將非常適合形式化陳述和證明這些屬性。透過這種方式，數學驗證 AI 生成程式碼的正確性將使其使用起來更安全。
Ono 總結道：「世界即將運行在沒有人閱讀過的電腦程式碼上。AI 已經到來，我們不能再視而不見，證明形式化是解決我認為我們將面臨的 AI 最重要挑戰的試驗場。」
