Axiom 把整部 Stacks Project 寫成 Lean 程式碼
美國 AI 數學初創 Axiom Math 11 月 5 日發布 Stacks Project 的 Lean 形式化版本，把這部約 7,500 頁的代數幾何參考著作，轉寫成約 1,600 萬行可由電腦核對的程式碼。Lean 是一種證明輔助語言：數學家把證明寫成程式碼，再由程式逐步檢查每一步推論是否成立。
Stacks Project 由哥倫比亞大學數學家 Johan de Jong 在 2005 年發起，是開放原始碼的參考著作，二十年來由數百名數學家補充證明和例子，每個定義和定理都有一個永久的四字元標籤。Axiom 的版本建於 Lean 社群的數學庫 Mathlib 之上，保留了這些標籤，研究人員可直接在新證明中引用當中的定義和定理。Axiom 稱，這是史上規模最大、可重複使用的整合式形式化數學庫。
AI 代理分工並行，找出原著數十處問題
據 Axiom 網誌，團隊設計了分層的 AI 代理系統，大批代理沿着定理之間的依賴關係並行工作，負責翻譯命題、在 Mathlib 搜尋現成定義、構建證明，同時保持各章的定義一致。Axiom 技術人員 Ashvin Swaminathan 向 TechCrunch 表示，代理會自行找出可以並行處理的工作。
Axiom 表示，系統在過程中找出 Stacks Project 內數十個需要修正的命題，包括缺少假設、正特徵下的邊界情況，以及在原文所述的一般情況下並不成立的說法。代理會構建反例，指出原命題在哪裡出錯，再補上缺漏的假設；若一條錯誤的輔助引理影響更深層的定理，代理會從文獻中另找路徑，在原有假設下完成證明。
AI 寫的部分仍待人手審核
項目網站顯示，程式庫分為兩部分：StacksCore 是已由人手對照原著核對、達到 Mathlib 標準的程式碼；StacksFrontier 則由 AI 代理編寫，尚未經人手審核。Lean 會檢查兩部分的每一個證明。Axiom 邀請外界審核 StacksFrontier 的程式碼，再移入 StacksCore，目標是日後把盡量多的內容併入 Mathlib。
項目 | 數字 |
|---|---|
Stacks Project 篇幅 | 約 7,500 頁 |
Lean 程式碼 | 約 1,600 萬行 |
Stacks Project 發起年份 | 2005 年 |
Axiom 估值（據 TechCrunch） | 16 億美元 |
Axiom A 輪融資（據 TechCrunch） | 2 億美元 |
行政總裁：起初不肯定 AI 寫得出來
據 TechCrunch 報道，Axiom 今年 3 月完成由 Menlo Ventures 領投的 2 億美元 A 輪融資，估值 16 億美元。25 歲的行政總裁 Carina Hong 曾在史丹福大學修讀數學博士，中途退學，2025 年 3 月創辦公司。
Carina Hong 向 TechCrunch 表示，團隊起初「不肯定 vibe coding 能否保留 Stacks 之美」。Vibe coding 指以自然語言描述需求，交由 AI 生成程式碼。她又向其他 AI 編程公司下戰書，表示「公開挑戰所有編程公司」做同等規模的形式化。Axiom 10 月 27 日亦發布了有限單群分類定理的 Lean 形式化。
暫時未有留言
提交留言即表示你已閱讀我們的私隱政策。