Axiom 將 Stacks Project 形式化為 1600 萬行 Lean 程式碼新
先了解這件事AI 綜述
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 則報導生成 · 更新
報導時間線
沿著報導，了解事件的不同側面；點標題看單篇報導的摘要與原文連結。
沒有符合條件的報導。
本事件熱度走勢
為什麼熱
過去 48 小時，有 2 個獨立來源報導，最近 6 小時新增 2 個。熱度 1.8，熱門榜第 6 名。
熱度以 48 小時內的獨立來源計，同一來源只算一次，每 24 小時權重減半。
事件紀錄
- 最早報導
- 最近更新
同一事件的報導集中在這裡，新的進展會繼續補充。