2026 年 11 月 5 日，Axiom（Axiom Math）宣布完成併發布 Stacks Project 的 Lean 形式化庫，把這部開源代數幾何基礎參考譯成約 1600 萬行可被機器逐行校驗的程式碼，稱其為迄今最大的一體化、可複用形式化數學庫。Stacks Project 由哥倫比亞大學數學家 Johan de Jong 於 2005 年發起，經數百位數學家二十年貢獻，內容從本科代數延伸到代數、幾何與數論前沿；據 TechCrunch 報導其規模約 7654 頁，Axiom 自己的表述為約 7500 頁。Axiom 稱部署了協同工作的 AI agent 叢集，並行翻譯、證明並整合數千條定理，TechCrunch 則強調定理之間的依賴關係保持完整。庫中每條 Lean 宣告都通過永久 Stacks 標籤回鏈原文，研究者和 AI agent 可直接匯入其中的定義與定理；代數幾何此前在 Lean 中幾乎空白。Axiom 由 25 歲的 Carina Hong 於 2025 年 3 月創辦，估值 16 億美元，已獲 Menlo Ventures 領投的 2 億美元 A 輪融資。公司稱，隨著 AI 生成數學論證的速度遠超人工檢查，形式驗證變得必要。對用 Lean、Mathlib 做形式化證明或讓 agent 生成數學程式碼的人來說，這提供了一個可直接複用的機器校驗基礎庫。
AI 根據 2 則報導生成 · 更新
沿著報導，了解事件的不同側面；點標題看單篇報導的摘要與原文連結。
Axiom 發布了整個 Stacks Project 的 Lean 形式化庫，約 1600 萬行，稱其為迄今最大的一體化、可複用形式化數學庫。該庫把這部約 7500 頁的代數幾何基礎參考變成單一機器校驗庫，研究者和 AI agent 可直接匯入定義與定理；每個 Lean 宣告都通過永久 Stacks 標籤回鏈原文。Axiom 表示，為完成這項工程，它部署了協同工作的 AI agent 叢集，並行翻譯、證明並整合數千條定理。
Axiom Math 宣布已完成 Stacks Project 的形式化驗證：AI agent 把這套約 7654 頁的數學文獻譯成約 1600 萬行可被 Lean 逐行檢查的程式碼，並保持定理之間的依賴關係完整。Stacks 覆蓋從本科代數到代數幾何、數論前沿的內容，而代數幾何此前在 Lean 中幾乎是空白。這家估值 16 億美元的初創由 25 歲的 Carina Hong 於 2025 年 3 月創辦，已獲 Menlo Ventures 領投的 2 億美元 A 輪融資；
過去 48 小時，有 2 個獨立來源報導，最近 6 小時新增 2 個。熱度 1.9，熱門榜第 5 名。
熱度以 48 小時內的獨立來源計，同一來源只算一次，每 24 小時權重減半。
同一事件的報導集中在這裡，新的進展會繼續補充。