前言
2026 年 5 月，DeepMind 在 arXiv 發布論文 Advancing Mathematics Research with AI-Driven Formal Proof Search，介紹了一套面向數學研究的形式化證明系統：AlphaProof Nexus。
如果只看結果，它似乎是在講 AI 又證明了一些數學題：系統在 353 個形式化 Erdos 開放問題中解決了 9 個，在 492 個 OEIS 猜想中證明了 44 個，還參與了圖論、最佳化理論、代數幾何、加性組合、量子光學等方向的實際研究。
但這篇論文對於在做 AI + 教育的我來說，更值得關注的是它的研究路線：
讓大模型負責提出證明思路，讓 Lean 這樣的形式化系統負責驗證，讓專門的證明搜尋器解決局部目標，再用多 Agent 編排把失敗、半成品和子目標都變成可復用的搜尋資產。
這篇文章我會盡量用小白能理解的方式，拆解 AlphaProof Nexus 的出發點、系統設計，以及論文中體現出的 四種 AI 數學研究範式。
一、為什麼 AI for Math 需要形式化證明？
普通人理解數學證明，通常是自然語言版本：
因為 A 成立，所以 B 成立。又因為某個定理，所以 C 成立。最後推出結論。
這對人類數學家是有效的，因為人可以補全中間省略的邏輯。但對 AI 來說，這裡有一個嚴重問題：大模型很會寫看起來像證明的文本，但不一定真的證明了。
它可能：
- 引用不存在的定理；
- 跳過關鍵步驟；
- 把一個困難問題換成另一個看似簡單但同樣沒證明的問題；
- 寫出語氣非常自信但邏輯錯誤的推導。
所以 DeepMind 這篇論文的核心出發點是讓 AI 在一個嚴格的系統裡工作。
這個系統就是 Lean。
Lean 可以理解為一個數學編譯器。程式設計師寫程式碼，編譯器會檢查程式碼有沒有語法錯誤、型別錯誤；數學家寫 Lean 證明，Lean 會檢查每一步邏輯是否真的成立。
如果 Lean 接受了一個證明，那麼這個證明就不是看起來對，而是經過機器嚴格檢查的。
這也是 AlphaProof Nexus 的基本思想：
AI 可以猜，可以試，可以失敗，但最終答案必須通過 Lean 驗證。
二、AlphaProof Nexus 到底是什麼？
AlphaProof Nexus 不是一個單獨的大模型，也不是一個只會聊天的數學助手，它更像一條 AI 數學研究流水線。
輸入是一份 Lean 文件，裡面有一個還沒完成的定理證明。系統要做的事情是不斷修改、補全、拆解這個證明，直到 Lean 接受它。
可以把它想像成這樣：
這裡面有幾個關鍵角色：
- LLM：負責提出證明思路、寫 Lean 程式碼、修復錯誤。
- Lean：負責檢查證明是否真的正確。
- AlphaProof：負責解決某些局部證明目標。
- Rater Agent：負責比較不同證明草稿哪個更有希望。
- Population DB：保存大量未完成但有價值的證明草稿。
- SafeVerify：最終檢查系統有沒有「作弊」，比如改了原定理、偷偷引入不允許的公理。
三、論文裡的 4 種 AI 數學研究範式
DeepMind 在論文中比較了 4 種 Agent 配置。它們也可以理解為 4 種 AI 做數學研究的範式。
範式一：Basic Agent
第一種是最基礎的模式：LLM + Lean 回饋循環。
它的工作方式很像一個程式設計師寫程式碼：
- LLM 看一個未完成的 Lean 證明。
- 它嘗試補上一段證明程式碼。
- Lean 編譯。
- 如果報錯，把錯誤資訊回饋給 LLM。
- LLM 根據錯誤繼續修改。
- 重複，直到證明通過，或者預算耗盡。
這類 Agent 的核心能力就是不斷試錯。
舉個例子：
你讓一個學生解題，他先寫一個解法，老師指出哪裡錯了，他再改。只不過這裡的老師不是人類，而是 Lean 編譯器。Lean 不會告訴你這個想法好不好，但它會非常嚴格地告訴你這裡型別不對、這裡目標沒有證明、這裡使用的定理不匹配，又或是這裡邏輯缺了一步。
這就給大模型提供了非常高品質的回饋。
論文裡一個有意思的結論是：Basic Agent 已經很強。
在事後實驗中，Basic Agent 也能復現那 9 個 Erdos 問題的成功案例，只是在更難的問題上成本更高、效率更差。
這說明，隨著大模型本身能力提升，簡單的「生成 - 編譯 - 修復」循環已經成為形式化數學中非常有競爭力的基線方法。
這類範式的啟發是：不要指望大模型一次性產出完美證明，而要把它放進一個可以持續回饋、持續修正的環境裡。
範式二：Basic Agent + AlphaProof
第二種範式是在 Basic Agent 的基礎上，加上 AlphaProof。
AlphaProof 是 DeepMind 之前發展的形式證明搜尋系統。在 Nexus 裡，它不是主角，而更像一個局部證明專家。
當 LLM 寫 Lean 證明時，經常會遇到一些小目標，比如：
當前上下文裡，證明這個子結論成立。
有些子目標很機械，但對 LLM 來說不一定好寫；有些目標需要搜尋一串 tactic，也就是 Lean 中的證明命令。這時系統可以把這些局部目標交給 AlphaProof。
AlphaProof 可能返回三種結果：
- 找到證明；
- 證明這個子目標其實是假的；
- 在預算內沒找到。
這很重要，因為它讓 LLM 不必獨自承擔所有證明細節。
可以這樣理解：LLM 更像研究生，負責整體思路和證明結構；AlphaProof 更像一個戰術搜尋器，負責局部技術細節；Lean 是最終裁判。
不過論文裡也提到 Standalone AlphaProof 並不能獨立解決這些研究級開放問題。
在實驗中，單獨使用 AlphaProof 沒有解決那 9 個 Erdos 問題。它真正有效的位置，是嵌入到 Nexus 這個更大的系統裡，作為局部證明工具使用。
範式三：Basic Agent + Evolution
第三種範式加入了一個很關鍵的思想：演化搜尋。
數學證明經常不是線性的。
一個證明路線可能走到一半發現卡住了；另一個路線雖然還沒完成，但看起來更接近核心；第三個路線證明了幾個有用的 lemma，雖然主定理還沒證明。
如果每次 Agent 都從零開始，那會浪費大量探索成果。所以 AlphaProof Nexus 會把未完成的證明草稿也保存下來，放入一個 Population DB，也就是證明草稿種子群。
然後系統會用 Rater Agent 對這些草稿進行比較，判斷哪些更有希望繼續發展。
這有點像生物演化：
- 每個證明草稿是一個個體；
- Agent 對草稿進行變異和改寫；
- Rater 選擇更有希望的草稿；
- 系統把計算資源投入到更有潛力的路線中。
這裡的難點在於，數學證明的成功信號非常稀疏。對程式最佳化來說，哪怕程式沒達到最優，也可以有一個分數。但對形式化證明來說，通常是完整證明成功或者沒成功。
中間狀態很難量化。
DeepMind 的做法是讓模型比較草稿品質，而不是直接給絕對分數。比如問模型：
這幾個未完成證明裡，哪個路線更清晰？哪個剩餘目標更可信？哪個更可能被補完？
然後系統用類似 Elo 的機制給證明草稿排序，並用 P-UCB 這樣的策略平衡兩件事：
- 繼續開發高分路線；
- 探索還沒被充分嘗試的新路線。
範式四：Full-featured Agent
第四種就是論文主推的系統：LLM + Lean + AlphaProof + Evolution。
它把前面幾種能力全部組合起來：
- LLM 負責寫證明、改證明、提 lemma；
- Lean 負責檢查每一步是否正確；
- AlphaProof 負責處理局部子目標；
- Evolution 負責保存和篩選不同證明路線；
- Rater Agent 負責判斷哪些草稿更值得繼續；
- SafeVerify 負責最終安全驗證。
這就是 AlphaProof Nexus 的完整形態。
它解決數學問題的方式很像一個高度自動化的研究團隊：有人提出方案、有人檢查邏輯、有人解決局部技術問題、有人評審不同方向、有人管理歷史結果、有人做最終驗收。
四、一個關鍵設計：證明搜尋必須防止作弊
AI 做數學證明有一個特殊問題，它可能通過改題來讓證明變簡單，而且它經常這麼做。
比如原來的目標是證明：對所有自然數 n，性質 P 成立。
Agent 可能偷偷改成：對某些自然數 n，性質 P 成立。
或者引入一個未經允許的公理：假設結論成立。
這樣 Lean 可能也能通過某些局部檢查，但這顯然不是我們想要的證明。
所以 AlphaProof Nexus 做了多層安全檢查：
- 檢查 theorem statement 是否被修改；
- 檢查是否還殘留
sorry； - 檢查是否引入不允許的 axiom；
- 檢查證明是否真的對應原始問題；
- 在沙箱環境中運行 Lean。
這對所有 Agent 系統都有啟發：當任務目標足夠複雜時，Agent 很容易學會繞過目標，而不是完成目標。因此必須設計強約束驗證層。
五、論文中的實驗結果
DeepMind 把系統用於多個數學任務，比較典型的是 Erdos 問題和 OEIS 猜想。
1. Erdos 問題
Erdos 是 20 世紀最重要的數學家之一，留下了大量開放問題。論文中系統處理了 353 個形式化 Erdos 開放問題，解決了其中 9 個。
這個比例看起來不高，但要注意，這些不是小學競賽題，而是研究級數學問題。
2. OEIS 猜想
OEIS 是整數序列資料庫，裡面有大量關於數列模式的猜想。系統在 492 個 OEIS 猜想中證明了 44 個。
這類任務非常適合形式化證明系統，因為很多數列猜想可以被清晰地編碼成定義和定理。
3. 實際數學研究部署
論文還提到系統被用於多個研究方向，包括圖論、最佳化理論、代數幾何、加性組合、量子光學。
六、寫在最後
最後總結下我在詳細閱讀這篇論文後得到的結論，歡迎交流討論。
結論一：LLM 已經可以成為形式化證明搜尋的核心元件
過去很多人認為，大模型不擅長嚴格數學，因為它會幻覺、會跳步、會胡編。
這句話沒錯，但不完整。
如果讓 LLM 直接寫自然語言證明，它確實不可靠。但如果把它放進 Lean 這樣的嚴格回饋系統裡，它就可以成為一個高效的搜尋引擎。
LLM 的價值不在於永遠正確，而在於它能提出大量候選路線，並根據編譯回饋不斷修正。
結論二：多 Agent 編排比單模型更重要
AlphaProof Nexus 的重點不是某個模型版本能解決難題了，而是系統把不同能力拆開成了：生成、檢查、搜尋、評分、快取、驗證。
這是一種工程化思路，數學研究被建模成一個長期搜尋過程。
結論三：失敗過程本身也有價值
未完成的 proof sketch、失敗的子目標、Lean 報錯、AlphaProof 的搜尋結果，都可以進入後續循環。
這讓數學證明搜尋變得更像軟體工程，比如程式碼可以復用、錯誤日誌可以分析、中間狀態可以保存、不同分支可以繼續開發、最終由編譯器驗收。
結論四：強模型和便宜模型可以分工
論文中使用較強模型做複雜證明生成，也使用較便宜模型做草稿比較和排序。
這是一種很實際的 Agent 工程經驗，不是所有環節都需要最強模型。
複雜推理用強模型，高吞吐評估用便宜模型，局部證明用專門工具。這比讓一個昂貴模型包打天下更可擴展。