Axiom Math 用 AI agents 正式驗證 Stacks Project，1,600 萬行程式碼

近幾個月數學圈有個怪現象：AI 好似每週都「開」一次數學難題。上月單係 OpenAI 就放出 719 份手稿，聲稱解答咗領域入面最棘手嘅問題。多年 AI 垃圾內容之後，有冇可能連數學都係下一個被淹沒嘅領域？呢個疑問唔係冇道理。

AxiomMath 嘅答案：唔好等，先要自己係地基。

做咗乜

公司今個星期三宣佈，佢嘅 AI agent 隊已將 Stacks Project 完成正式驗證（formal verification），轉換成約 1,600 萬行經程式碼助手逐行檢查嘅 Lean 程式碼。

Stacks Project 由哥倫比亞大學數學系 Johan de Jong 於 2005 年創始，係一個開放源碼數學參考庫，由大學代數一直延伸至最尖端嘅代數幾何與數論。哥倫比亞數學家 Peter Woit 稱「冇乜嘢真正可比擬」，將佢同喺 20 世紀重建數學基礎嘅 Bourbaki 書係放落一齊睇。

Axiom 嘅 AI agents 將約 7,654 頁嘅內容翻成約 1,600 萬行程式碼。技術人員 Ashvin Swaminathan 話團隊為 agents 設了層次架構，但唔係完全指令式：「agents 自己揾任務，再識辨邊啲嘢可以並行處理。」佢哋嘅做法亦包括自訓數學模型，由一名內部 Lean 專家先「教」agents 人嘅判斷力。

點解要用呢個方法

正式驗證唔等同自動寫定理。數學家用 Lean 程式語言將證明重寫成程式碼，再由證明助手逐行核對邏輯。呢個做法早喺晶片設計、以至法國研究人員攞去抓福利計算軟體入面嘅錯誤。

但對 Stacks 呢種規模，逐條定理驗證唔夠。Stacks 嘅定理同定義互相依戀，好似一棵家譜，大量結果可追溯返去之前嘅定理。CEO Carina Hong（25 歲，Stanford 數學 PhD 中輟，2025 年 3 月創辦公司）講：「大嘅嘢同需要小心處理嘅嘢喺人生入面從來冇一齊出現過。你希望定理一致、唔會出現矛盾，希望定義互相唔會打架。」

Axiom 估值 16 億美元；2025 年 3 月 Menlo Ventures 領投 A 輪 2 億美元。公司目標係為 AI agents 建一個「已驗證嘅地基」，俾佢哋寫軟件、甚至日後做科學。