2026 年 11 月 5 日，Axiom（Axiom Math）宣布完成併發布 Stacks Project 的 Lean 形式化庫，把這部開源代數幾何基礎參考譯成約 1600 萬行可被機器逐行校驗的程式碼，稱其為迄今最大的一體化、可複用形式化數學庫。Stacks Project 由哥倫比亞大學數學家 Johan d… 看完整事件
Axiom 發布 Stacks Project 的 Lean 形式化庫，約 1600 萬行
Axiom 發布了整個 Stacks Project 的 Lean 形式化庫，約 1600 萬行，稱其為迄今最大的一體化、可複用形式化數學庫。該庫把這部約 7500 頁的代數幾何基礎參考變成單一機器校驗庫，研究者和 AI agent 可直接匯入定義與定理；每個 Lean 宣告都通過永久 Stacks 標籤回鏈原文。Axiom 表示，為完成這項工程，它部署了協同工作的 AI agent 叢集，並行翻譯、證明並整合數千條定理。
這是代數幾何基礎參考首次被整體形式化，1600 萬行規模超過以往形式化數學庫，且由 AI agent 叢集並行完成；對 Lean/Mathlib 使用者和關注 AI 數學驗證的人有直接價值。
原標題：The Stacks Project, Formalized in Lean
閱讀原文
| 評分 | 82 / 68（平均 75，門檻 76） |
|---|---|
| 狀態 | 未入選 |
相關報導
Anthropic 用 Lean 自動形式化費馬大定理，11 天生成 1300 萬行
數學形式化正從人工轉錄轉為 AI 自動形式化：Anthropic 於 2026 年 9 月 4 日宣布完成費馬大定理的自動形式化，11 天生成 1300 萬行 Lean 程式碼；OpenAI 9 月 8 日公布 Navier-Stokes 強制爆破定理時也附帶了 Lean 形式化。此前 Math Inc. 在 24 維球填充問題上生成約 50 萬行程式碼，Meta 的 ATLAS 專案則自動形式化了 26 本教科書的大部分內容。
數十個 AI Agent 用 24 天完成有限單群分類定理的 Lean 形式化
10 月 26 日，Axiom Math 宣布數十個 AI Agent 用 24 天完成了有限單群分類定理的 Lean 形式化，產出約 4310 萬行程式碼、205 萬個宣告。這項被稱「巨型定理」的證明由 100 多位數學家耗費數十年寫成，約 1.5 萬頁、散落在 500 多篇論文裡。過程中 Agent 發現 1986 年 Walter 不平衡群定理的一處推理漏洞，並在群論專家建議下構造出新定理 Preservation of simple tops 補上這條路線。
論文：Lean 驗證 AI 形式化證明不等於原證明正確
arXiv 新論文指出，用 Lean 機械驗證 AI 自動形式化的數學證明，並不能保證原始自然語言證明本身正確。作者 Bastounis、Circelli 與 Hansen 證明，要做到語義忠實的翻譯必須消解自然語言數學文字的歧義，而該問題在可解複雜度指數（SCI）層級中為無窮，比停機問題（SCI=1）更難。
@AnthropicAI: New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Anthropic 前沿紅隊部落格發布研究：與 Theorem Labs 合作，用 Claude 在數週內為一百多個真實開源庫證明安全屬性。形式化驗證過去只能用於小規模程式碼庫或需大量專家時間，AI 模型正讓大規模驗證變得可行。完整研究已在其部落格發布。
評論：AI 借 Lean 寫數學證明，不讀 AI 程式碼漸成常態
一位電腦科學家在這篇評論中指出，AI agent 結合 Lean 等互動式證明助手，正在把希爾伯特百年前設想的「證明機器」變為現實，其對數學界的衝擊甚至超過希爾伯特綱領的失敗。他同時警告，程式設計領域已把不讀 AI 生成程式碼當成常態；而在 Curry-Howard 對應下程式與證明本質相同，放棄閱讀就等於放棄理解。他主張像數學家反覆簡化 AI 證明那樣，用抽象、重構與更高層語言把程式碼簡化到能裝進腦中。