編輯｜Panda

數(shù)學(xué)正在迎來 AI 革命。

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

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

現(xiàn)在，新的進展來了！Meta 聯(lián)合紐約大學(xué)等機構(gòu)正式發(fā)布了ATLAS（Autoformalized Textbook Library At Scale），一項迄今為止規(guī)模最大的自動化數(shù)學(xué)形式化工程之一。

項目論文和代碼都已發(fā)布。

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

什么是 ATLAS？

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

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

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

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

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

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

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

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

用戶可以在其中：

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

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

來自哪些教科書？

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

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

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

核心引擎：AutoformBot

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

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

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

整個系統(tǒng)分為三個管理層級：

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

值得強調(diào)的是：整個 ATLAS 的生成過程零人工證明工程介入，完全由機器自動驅(qū)動。這既是其宏大規(guī)模得以實現(xiàn)的前提，也是需要持續(xù)改進質(zhì)量和可靠性的原因。

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

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

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

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

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

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

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

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

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

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

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

局限性

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

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

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

• 完成各書中剩余定理的形式化；
• 納入更多教材和數(shù)學(xué)領(lǐng)域；
• 提升代碼質(zhì)量與可維護性；
• 向 Mathlib 規(guī)范靠攏，爭取更廣泛的開源兼容發(fā)布。

亦歡迎外部貢獻者。

結(jié)語

ATLAS 的發(fā)布，恰好呼應(yīng)了近期數(shù)學(xué)界最重要的一場認知轉(zhuǎn)變。

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

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

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

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

從這個角度看，ATLAS 的意義超越了一個代碼倉庫的范疇：它是一次對「數(shù)學(xué)基礎(chǔ)設(shè)施」的大規(guī)模投資實驗。