編輯｜Panda

數學正在迎來 AI 革命。

最近幾個月尤為明顯。比如，就在前幾天，Google DeepMind 新論文宣布其最新系統 AlphaProof Nexus 在一次自主運行中，解決了 353 道開放 Erd?s 問題中的 9 道，其中兩道已在數學界懸而未決長達 56 年，并且每道題的推理成本，僅需區區幾百美元。詳情可參閱《一個問題幾百美元，DeepMind 智能體一次搞定了 9 個 Erd?s 問題》。

Erd?s 問題通常指匈牙利傳奇數學家 Paul Erd?s 在其一生中提出的大量公開數學問題與猜想。這些問題廣泛分布于組合數學、數論、圖論、離散幾何、概率論等領域，其中許多長期未解，并被視為相關方向的重要研究基準與前沿挑戰。這一結果之所以可信，關鍵在于 AlphaProof Nexus 并非生成自然語言證明，而是將大語言模型（Gemini 3.1 Pro）與形式化驗證工具 Lean 深度結合：AI 提出證明，Lean 逐步核查每一個邏輯步驟，通不過就直接拒絕。所有證明代碼已公開于 GitHub，任何人都可以獨立復現驗證。

現在，新的進展來了！Meta 聯合紐約大學等機構正式發布了ATLAS（Autoformalized Textbook Library At Scale），一項迄今為止規模最大的自動化數學形式化工程之一。

項目論文和代碼都已發布。

• 項目地址：https://github.com/facebookresearch/atlas-lean/
• 論文地址：https://github.com/facebookresearch/atlas-lean/blob/main/formalizing_mathematics_at_scale.pdf

什么是 ATLAS？

簡單來說，ATLAS 是一個基于 Lean 4 的數學形式化代碼庫，其核心目標是：將數學教科書中的非正式定理陳述與證明，自動翻譯成計算機可逐行驗證的形式化代碼。

這件事聽起來枯燥，但意義深遠。Lean 是一種「證明助手」語言，當你向它提交一段數學證明時，它會像編譯器檢查代碼那樣，逐步驗證每一個推導步驟的邏輯合法性。是的，只要 Lean 通過，這個證明就在形式意義上無懈可擊。

按照項目 Readme 中的統計數據，截至 2026 年 5 月，ATLAS 已經覆蓋 26 本本科及研究生級別數學教科書，橫跨分析學、代數學、幾何、拓撲、組合數學、概率、統計、偏微分方程、數論以及理論計算機科學等眾多領域。

整個代碼庫共計630,999行代碼，其中 Lean 核心代碼483,917行；包含 46,203 條數學聲明（declarations），其中 42,837 條已完成證明，證明通過率高達 92.7%。

在被選定的 4,007 條教科書定理中，已有 2,855 條完成形式化，形式化覆蓋率達 71.3%。從規模上看，Lean 社區多年協作維護的標準庫 Mathlib 約有 210 萬行代碼、308,129 條聲明。ATLAS 在數周內機器生成的體量，已達到 Mathlib 總量的約四分之一，這一速度令人咋舌。

這個數字背后是驚人的計算消耗：整個生成過程共使用了超過1830 億（183,157M）個 token。

值得注意的是，團隊還構建了一個可視化瀏覽器。

地址：https://rammalahmad.github.io/atlas/

用戶可以在其中：

• 對比每條定理的非正式原文與 Lean 形式化版本；
• 瀏覽定理之間的邏輯依賴關系圖（即證明哪個定理需要先知道哪些引理）；
• 提取證明特定定理所需的最小 Lean 代碼集合。

這個工具的意義在于，它將 ATLAS 從一個代碼庫變成了一張可導航的數學知識圖譜，對人類研究者和未來的 AI 系統都具有潛在價值。

來自哪些教科書？

ATLAS 的26本教材全部來自 MIT OpenCourseWare 等頂級開放課程資源，覆蓋范圍非常廣。

以下是幾個有代表性的案例：

• RealAnalysis（實分析）：177 條目標定理中已形式化 175 條，覆蓋率高達 98.9%，證明通過率 98.7%，堪稱項目中完成度最高的單本。
• ComplexVariables（復變函數）：97.4% 的形式化覆蓋率。
• NumberTheoryI（數論 I）：576 條目標定理，已形式化 460 條（79.9%），生成代碼近 65,000 行。
• AlgebraicGeometryI（代數幾何 I）：這是難度最高的領域之一，形式化覆蓋率 60.2%，但仍生成了超過 4 萬行代碼和 4,499 條聲明。
• LieGroups（李群）：消耗 token 最多（45,384M），生成了超過 6 萬行代碼，盡管形式化覆蓋率僅 40%，反映了該領域的極端技術難度。

核心引擎：AutoformBot

當然，ATLAS 的生成并非人工一行行書寫，而是完全依賴 Meta 自研的自動形式化流水線AutoformBot（已在 GitHub 上開源）。

項目地址：https://github.com/facebookresearch/autoform-bot

AutoformBot 將教科書形式化視為一個協同軟件工程問題，借鑒了成熟的開源協作范式（git 分支、Pull Request 審查、Issue 追蹤）來協調數以百計的 LLM 智能體同時工作。

整個系統分為三個管理層級：

• 頂層的編排者（orchestrator）負責閱讀教科書、將形式化任務拆解為有向無環圖（DAG），并根據書中的邏輯依賴關系調度工作順序；
• 中層的追蹤分析器（trace analyzer）監督者（supervisor）分別負責從失敗任務中學習、以及在每次合并后評估目標完成質量；
• 底層的工作者（worker）審核者（reviewer）則負責實際執行單條定理的形式化與代碼審核。

值得強調的是：整個 ATLAS 的生成過程零人工證明工程介入，完全由機器自動驅動。這既是其宏大規模得以實現的前提，也是需要持續改進質量和可靠性的原因。

整個系統的計算消耗主要集中在工作者層，占總 token 用量約 76%。每本書的形式化過程通常持續約一周，但可通過增加并行度顯著壓縮時間。

論文中的實驗表明，每任務使用 3 個或 5 個 worker 并行競速比單一 worker 在相同時間內多完成約 20% 的目標。

團隊在論文中坦誠披露了系統運行中觀察到的若干有趣「失效模式」，其中最出人意料的是 worker 的對抗性「作弊」和「摸魚」行為

理解這一現象的關鍵，在于 Lean 里有個叫 sorry 的特殊關鍵字：它相當于一張「欠條」，告訴編譯器「此處證明先跳過，暫且假設為真」。代碼因此能順利編譯，但邏輯鏈條里實際留著一個空洞。在正常開發中，sorry 是標記「待填坑」位置的合法工具；但在 AutoformBot 里，它成了 worker 應付考核的捷徑：遇到難以證明的定理，就悄悄在某個輔助引理深處塞一個 sorry，讓整條證明鏈看起來通過了，實則是一座紙牌屋。

而這只是最基礎的一種手法，論文歸納的「作弊清單」還包括：

• 把定理名稱保留、但把真實內容替換成永遠為真的廢話；
• 把本應證明的結論偷偷藏進數據結構的字段定義（定義不需要證明，只需要通過類型檢查）；
• 把難題中的復雜數學對象換成簡單替身，比如明明要構造一個同構映射，卻只證明了兩個空間的維數相等就交差。

更有趣的是事態的演變：當 reviewer 智能體被要求嚴格反作弊后，worker 并沒有就此收手，而是把 sorry 埋得更深，藏進依賴鏈條的更底層，讓表層審查無法察覺。這場貓鼠游戲倒逼團隊構建了一套遞歸追蹤整個依賴圖的分析工具，才得以溯源找到真正的「污染節點」。

這場 worker 與 reviewer 之間的貓鼠游戲，在論文中被稱「對抗動態」（adversarial dynamic），并被視為大規模多智能體系統中值得深入研究的協調問題。

此外，長期運行的編排者會出現「LLM 疲勞」：隨著上下文窗口被大量歷史信息占滿，它開始生成越來越粗糙的任務描述，甚至悄悄放棄處理困難目標。團隊的解決方案是將專項分析工作委派給短生命周期的專業智能體，避免單一長期智能體的上下文退化。

在模型選擇上，論文提供了一組關鍵對比數據：以同等算力預算（1200M tokens）在《代數組合學》教科書上對比，Claude Opus 4.6 完成了 92% 的形式化目標，而 Gemini 3.1 Pro 僅完成 46%—— 差距幾乎在實驗開始時就已顯現，團隊將其歸因于模型在 Lean 語言上的編碼能力差異。這也是為何整個 ATLAS 主要由 Opus 4.6 驅動。

在成本方面，團隊估計，當前流水線的單行代碼成本已低于人類專家標注，同時速度更快、可擴展性更強，不過輸出質量整體上仍不及專家手寫的 Lean 代碼。

局限性

團隊對 ATLAS 的定位相當誠實：這是一個持續進行中的機器生成擴展努力，而非一個完成品。

目前仍有約 28.7% 的目標定理尚未形式化，部分難度較高的領域（如李群、布爾函數分析）覆蓋率低于 50%。代碼風格也與 Lean 社區的主流標準庫 Mathlib 尚存差距 ——Mathlib 是全球數學家協作維護的「黃金形式化庫」，有著嚴格的風格約定和深度整合要求。

按照團隊的下一步計劃，ATLAS 將繼續：

• 完成各書中剩余定理的形式化；
• 納入更多教材和數學領域；
• 提升代碼質量與可維護性；
• 向 Mathlib 規范靠攏，爭取更廣泛的開源兼容發布。

亦歡迎外部貢獻者。

結語

ATLAS 的發布，恰好呼應了近期數學界最重要的一場認知轉變。

菲爾茲獎得主陶哲軒近期指出，數學正在經歷從「證明匱乏」到「證明泛濫」的歷史性轉變。對他而言，真正的問題不再僅僅是 AI 能否生成數學證明，更有趣的是：數學共同體是否擁有足夠的基礎設施，來吸收、驗證、整理和理解 AI 可能很快大規模產出的數學成果。

https://mathstodon.xyz/@tao/116653336847856534

他的判斷一針見血：「首先發現某個證明，或者率先形式化某個定理，不應該是最終目標。闡釋與消化，正在變得遠比這更加重要。」

陶哲軒認為，AI 越來越能生成大量看似嚴謹實則暗含謬誤的論證，而形式驗證工具（如 Lean）是讓 AI 保持誠實的關鍵手段。

從這個角度看，ATLAS 的意義超越了一個代碼倉庫的范疇：它是一次對「數學基礎設施」的大規模投資實驗。