感覺人工智能幾乎每週都在攻克一個新的數學難題。上個月，僅 OpenAI 一家就發布了 719 篇手稿，聲稱解決了該領域一些最困難的問題。即使是電腦檢查也可能出錯。在經歷了多年 AI 垃圾內容之後，人們不禁會問，數學會不會成為下一個受影響的領域。
AxiomMath 透過建立更堅實的基礎，而非放慢速度，來避開這種命運。這家估值 16 億美元的初創公司希望打造一個經過驗證的基礎層，讓 AI 代理能夠依賴它來編寫軟體，並最終從事科學研究。
週三，該公司宣布已正式驗證 Stacks Project，這是人類寫下的最大數學成果之一。數學家們通常對 Stacks 評價極高。哥倫比亞大學數學家 Peter Woit 曾稱它「幾乎沒有別的東西能與之相比」，並把該項目比作「著名的 Bourbaki 書叢」——那套在 20 世紀從基礎重建數學的系列著作。
Woit 的哥倫比亞同事 Johan de Jong 於 2005 年啟動了 Stacks Project，作為一個開源參考資料。此後，數學家們一直為其貢獻內容，從大學水平的代數一路擴展到代數、幾何和數論等領域最前沿的思想。
該公司的 AI 代理群將這套約 7,654 頁的資料庫翻譯成約 1,600 萬行可由電腦檢查的代碼。
形式化數學的目的是確保其底層結構是可靠的。數學家會使用一種名為 Lean 的程式語言，將證明重寫為代碼，再由一個稱為 proof assistant 的程式逐行檢查這些代碼。如果證明通過，數學家就可以相信它在邏輯上是成立的。
工程師也使用同樣的思路，即形式化驗證，來確認晶片設計是否可行；法國的研究人員則用它發現了計算家庭補助的軟體漏洞。
對於像 Stacks Project 這樣的資料庫來說，逐個檢查定理只是工作的一部分。Stacks 中的定理和定義彼此關聯，每一個都建立在前面的內容之上。就像家譜一樣，Stacks 裡的許多結果都可以追溯到更早的結果。
這種相互關聯性讓 Axiom 一開始並不確定這個項目是否可行。團隊必須在約 1,600 萬行 Lean 代碼中保持每一處連接都完整無缺。
Axiom 首席执行官 Carina Hong 告訴 TechCrunch：「規模大和精細這兩件事在現實中通常並不相容。［Stacks］是一組構成數學基礎的數學成果。你希望［定理］彼此一致，而不是像有悖論一樣。你也希望這些定義之間不要互相衝突。」
這位 25 歲的 CEO 曾從史丹福大學數學博士項目退學，並於 2025 年 3 月創辦了這家公司。今年 3 月，Axiom 在 Menlo Ventures 領投下完成了 2 億美元 A 輪融資。
Hong 說：「我們當時並不確定 vibe coding 是否能保留 Stacks 的美感。」
為了完成這個項目，團隊為代理設定了一個鬆散的架構，並讓它們並行運行。Axiom 技術團隊成員 Ashvin Swaminathan 說：「對於 Stacks，我們設定了一個層級……但並不是那種完全規定每個代理具體做什麼的層級。代理會自行尋找任務，並識別出可以並行處理的事情。」
Axiom 還訓練了自己的模型，使其擅長數學。Hong 表示，這種做法是大多數其他驗證型初創公司未採取的。起初，團隊依賴一位內部 Lean 專家來教這些代理形成類似人類的判斷標準。隨著時間推移，Hong 說，這些代理已自行學會了這種判斷力。
這一成果填補了形式化數學中最大的空白之一。Swaminathan 說：「當你查看已被形式化的數學內容時，會發現有一個巨大的黑洞，而這個黑洞涵蓋了代數幾何。」
Swaminathan 表示，直到現在，想使用 Lean 檢查代數幾何新成果的研究人員幾乎沒有現成的基礎可用。「現在他們有了。」
Axiom 認為，每一個經過驗證的結果都將成為一塊積木，未來的證明可以建立在已檢查的數學基礎之上，而無需從頭開始。UCLA 數學家、菲爾茲獎得主 Terence Tao 用更簡潔的話概括了這一點：「你擁有的形式化證明越多，你就能做出越多形式化證明。」
Axiom 的目標受眾並不僅限於數學家。開發者長期以來一直致力於確保其代碼沒有漏洞和安全隱患。隨著 AI 代理編寫的軟體越來越多，這個問題只會變得更加嚴重。
Axiom 賭注，未來的軟體需要建立在經過驗證的基礎之上，就像如今的 Stacks 一樣。
Swaminathan 說：「我們認為，數學是你開始構建這些東西的領域，而且這是一項可遷移的技能。代理可以閱讀我們的代碼，理解它，並在其上構建新的基礎設施。我們用 Lean 做出的形式化，現在就是代理可以建立其上的底層基座。」
Axiom 代理構建 Stacks 的方式——並行工作、自行挑選任務——正是 Hong 預期未來許多 AI 工作的方式。她認為，AI 代理需要一個結構良好、可重用的知識庫，才能避免產出垃圾內容。
Hong 說：「你希望［代理］擁有一個可重用的資料庫，讓它們可以在上面繼續構建並不斷推進前沿。如果一開始就用糟糕的工程選擇把垃圾塞進去，那麼它們就很難再擴展那個邊界。」
Hong 對這種方法非常有信心，甚至公開下了戰書。她說：「我公開挑戰所有程式設計公司，都來做這種規模的形式化工作。」