感覺人工智能幾乎每週都在攻克一個新的數學難題。上個月，僅有 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 对於這種方法非常有信心，甚至公開下戰書。她說：「我公開挑戰所有編程公司，來做這種規模的形式化工作。」