消耗1830億token，Meta用AI把數(shù)學(xué)教材翻譯成了一個(gè)超大Lean庫(kù)

編輯｜Panda

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

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

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

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

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

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

什么是 ATLAS？

簡(jiǎn)單來(lái)說(shuō)，ATLAS 是一個(gè)基于 Lean 4 的數(shù)學(xué)形式化代碼庫(kù)，其核心目標(biāo)是：將數(shù)學(xué)教科書(shū)中的非正式定理陳述與證明，自動(dòng)翻譯成計(jì)算機(jī)可逐行驗(yàn)證的形式化代碼。

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

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

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

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

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

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

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

用戶可以在其中：

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

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

來(lái)自哪些教科書(shū)？

ATLAS 的26本教材全部來(lái)自 MIT OpenCourseWare 等頂級(jí)開(kāi)放課程資源，覆蓋范圍非常廣。

以下是幾個(gè)有代表性的案例：

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

核心引擎：AutoformBot

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

項(xiàng)目地址：https://github.com/facebookresearch/autoform-bot

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

局限性

團(tuán)隊(duì)對(duì) ATLAS 的定位相當(dāng)誠(chéng)實(shí)：這是一個(gè)持續(xù)進(jìn)行中的機(jī)器生成擴(kuò)展努力，而非一個(gè)完成品。

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

按照?qǐng)F(tuán)隊(duì)的下一步計(jì)劃，ATLAS 將繼續(xù)：

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

亦歡迎外部貢獻(xiàn)者。

結(jié)語(yǔ)

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

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

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

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

陶哲軒認(rèn)為，AI 越來(lái)越能生成大量看似嚴(yán)謹(jǐn)實(shí)則暗含謬誤的論證，而形式驗(yàn)證工具（如 Lean）是讓 AI 保持誠(chéng)實(shí)的關(guān)鍵手段。

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