2026 年 11 月 5 日，Axiom（Axiom Math）宣布完成併發布 Stacks Project 的 Lean 形式化庫，把這部開源代數幾何基礎參考譯成約 1600 萬行可被機器逐行校驗的程式碼，稱其為迄今最大的一體化、可複用形式化數學庫。Stacks Project 由哥倫比亞大學數學家 Johan d… 看完整事件
Axiom Math 將 Stacks Project 形式化為 1600 萬行 Lean 程式碼
Axiom Math 宣布已完成 Stacks Project 的形式化驗證：AI agent 把這套約 7654 頁的數學文獻譯成約 1600 萬行可被 Lean 逐行檢查的程式碼，並保持定理之間的依賴關係完整。Stacks 覆蓋從本科代數到代數幾何、數論前沿的內容，而代數幾何此前在 Lean 中幾乎是空白。這家估值 16 億美元的初創由 25 歲的 Carina Hong 於 2025 年 3 月創辦，已獲 Menlo Ventures 領投的 2 億美元 A 輪融資；
把代數幾何這一 Lean 形式化中的最大空白整體搬進機器可檢查的程式碼，1600 萬行規模遠超以往，對做形式化驗證、Lean 與 AI for math 的開發者最有參考價值。
原標題：Axiom Math wants to keep AI slop out of mathematics
閱讀原文
| 評分 | 80 / 67（平均 73，門檻 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 本教科書的大部分內容。
論文：Lean 驗證 AI 形式化證明不等於原證明正確
arXiv 新論文指出，用 Lean 機械驗證 AI 自動形式化的數學證明，並不能保證原始自然語言證明本身正確。作者 Bastounis、Circelli 與 Hansen 證明，要做到語義忠實的翻譯必須消解自然語言數學文字的歧義，而該問題在可解複雜度指數（SCI）層級中為無窮，比停機問題（SCI=1）更難。
數十個 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 補上這條路線。
OpenAI 一次公開 722 篇 AI 數學論文，僅 42% 完成形式化驗證
OpenAI 在 GitHub 公開了 722 篇由內部未發布前沿模型生成的數學手稿，涵蓋數論、代數幾何、分析、組合數學等方向，其中約 300 項核心結果完成 Lean 形式化驗證，佔 42%。公司稱模型共嘗試超過 4000 個問題，一項典型成果平均消耗約 3 小時 ChatGPT Pro thinking 算力，但未公開所用模型與提示詞。
評論：AI 借 Lean 寫數學證明，不讀 AI 程式碼漸成常態
一位電腦科學家在這篇評論中指出，AI agent 結合 Lean 等互動式證明助手，正在把希爾伯特百年前設想的「證明機器」變為現實，其對數學界的衝擊甚至超過希爾伯特綱領的失敗。他同時警告，程式設計領域已把不讀 AI 生成程式碼當成常態；而在 Curry-Howard 對應下程式與證明本質相同，放棄閱讀就等於放棄理解。他主張像數學家反覆簡化 AI 證明那樣，用抽象、重構與更高層語言把程式碼簡化到能裝進腦中。