北京
新智元報道
【新智元導讀】DeepMind發(fā)布全新數(shù)學智能體AlphaProof Nexus，9道Erd?s開放難題一次性告破，最老的懸了56年！全部證明都已經(jīng)過Lean編譯器形式化驗證，沒有幻覺。網(wǎng)友驚呼：數(shù)學奇點的火花點燃了。
數(shù)學界這個月，徹底瘋了。
前腳OpenAI剛把Erd?s 80年猜想推翻，數(shù)學家們的驚呼聲還沒落地。
緊接著，Google DeepMind發(fā)布了一個全新AI數(shù)學智能體——AlphaProof Nexus。
論文地址：https://arxiv.org/abs/2605.22763v1
它一出手，就干掉了9道懸而未決幾十年的Erd?s開放問題。其中最古老的那個，懸了整整56年！
而且，每道題花費的算力成本，只有幾百美元。
更關(guān)鍵的是，這次的證明不可能有錯。
每一步推理都經(jīng)過Lean編譯器的形式化驗證，不存在幻覺空間。編譯器通過，證明就是對的。
值得一提的是，AlphaProof Nexus和2024年拿下IMO銀牌的初代AlphaProof完全不同。
初代只有強化學習樹搜索，Nexus把大語言模型、AlphaProof和進化算法三合一，直接瞄準了人類數(shù)學家啃不動的研究級難題。
AlphaProof Nexus
進化算法+LLM+Lean編譯器
這套系統(tǒng)的架構(gòu)分為四個層級，從簡單到復雜。
1. Agent A（基礎(chǔ)版）
多個獨立的證明子智能體并行工作，每個子智能體與Gemini 3.1 Pro進行多輪對話，通過搜索替換工具修改Lean代碼，編譯器實時反饋錯誤信息，子智能體根據(jù)反饋迭代修正。
2. Agent B
在A的基礎(chǔ)上加入了AlphaProof作為工具。當子智能體在某個子目標上卡住時，可以調(diào)用AlphaProof進行強化學習驅(qū)動的樹搜索，嘗試攻克局部難點。
3. Agent C
引入進化算法。多個子智能體不再獨立工作，而是共享一個「種群數(shù)據(jù)庫」。每個證明草稿會被LLM評審員打分（用Elo評分系統(tǒng)），高分草稿被優(yōu)先采樣、變異、進化。
4. Agent D（完整版）
集大成者。進化算法 + AlphaProof + Gemini 3.1 Pro協(xié)同作戰(zhàn)。這是DeepMind用來大規(guī)模掃蕩Erd?s問題的主力武器。
整個工作流的核心循環(huán)非常清晰——
AI提出證明草稿 → Lean編譯器驗證 → 失敗則反饋錯誤信息 → AI修正 → 再驗證 → 循環(huán)往復，直到證明完全通過或耗盡算力預算。
以Erd?s #125為例，它的解題過程是這樣的。
首先，子智能體先用思維鏈推理分析問題結(jié)構(gòu)，然后通過搜索替換修改Lean代碼，接著調(diào)用AlphaProof處理子目標。
AlphaProof搞定了6個子目標中的3個，子智能體隨即將剩余的「硬骨頭」分解為更小的引理，再次調(diào)用AlphaProof——這次，全部搞定。
整個過程中，沒有任何人類數(shù)學家介入。
9道Erd?s問題
56年前的懸案一朝告破
DeepMind將完整版Agent D投放到353道已形式化的Erd?s問題上。每道題最多允許3000輪迭代。
最終，9道問題被攻克。
其中含金量最高的幾道：
1. Erd?s #12（1970年提出）
是否存在一個無限集A，滿足「任意三個不同元素a
這道題懸置了56年，期間多位數(shù)學家取得了部分進展，但始終無法給出完整構(gòu)造。
AI的解法精妙地結(jié)合了中國剩余定理和三項等差數(shù)列回避集，通過構(gòu)建一系列精心設(shè)計的「區(qū)塊」來同時滿足密度條件和整除約束。
2. Erd?s #125（1996年提出）
在三進制下只用數(shù)字0和1的整數(shù)集A，加上四進制下只用數(shù)字0和1的整數(shù)集B，它們的和集A+B的下密度是否為正？
AI證明了答案是否定的——下密度為零。
證明的核心是一個歸納稀疏化論證，巧妙利用了3^m和4^k的丟番圖逼近性質(zhì)（log4/log3是無理數(shù)），通過反復找到兩個基數(shù)幾乎對齊的尺度，讓密度以0.99的比率逐步衰減到零。
3. Erd?s #138（1981年提出的變體）
van der Waerden數(shù)W(k+1) - W(k)是否趨于無窮？
AI給出了一個極其優(yōu)雅的證明：W(k+1) ≥ W(k) + k。核心思路是貪心染色擴展——在一個沒有單色k-AP的2-著色基礎(chǔ)上，逐個添加新元素，用反證法說明貪心策略不會失敗。
4. Erd?s #846
這是一個關(guān)于平面點集中共線性質(zhì)的問題。
而AI的構(gòu)造，令人嘆為觀止。
它把完全圖K∞的每條邊映射到平面上的一個點，用二次多項式編碼坐標，然后利用無窮Ramsey定理完成證明。
目前，所有9道問題的Lean證明代碼已開源在GitHub上。
項目地址：https://github.com/google-deepmind/alphaproof-nexus-results
簡單Agent也能解全部9題？！
最出人意料的結(jié)論，不是完整版Agent D有多強，而是——
最簡單的Agent A，也能解決全部9道問題。
Agent A沒有進化算法，沒有AlphaProof，只有多個獨立的LLM子智能體和Lean編譯器的反饋循環(huán)。
根據(jù)DeepMind團隊的對比分析，它在大多數(shù)問題上，Agent A和Agent B（加了AlphaProof的版本）的表現(xiàn)在誤差范圍內(nèi)幾乎相同。
相比之下，Agent D的優(yōu)勢主要體現(xiàn)在最困難的問題上（比如#125和#138），能以2到5倍的成本優(yōu)勢完成證明。
對此，DeepMind將基礎(chǔ)Agent的成功歸因于兩個因素：LLM自身能力的飆升，以及編譯器反饋在錨定LLM推理方面的強大作用。
也就是說，隨著基礎(chǔ)模型越來越強，復雜的系統(tǒng)工程可能逐漸讓位于簡單的智能體循環(huán)。
今天需要進化算法和AlphaProof協(xié)同作戰(zhàn)才能高效解決的問題，明天可能一個樸素的LLM+編譯器循環(huán)就夠了。
具體到成本，最便宜的一道題（#741(ii)）中位成本僅5-7美元，最貴的（#152）也不過200-400美元。
但前提是用對了模型——單獨運行AlphaProof或使用較小模型（Gemini 3.0 Flash等），9道題一道都解不出來。
代數(shù)幾何15年懸案、凸優(yōu)化新界一并搞定
除了Erd?s問題，AlphaProof Nexus還在多個數(shù)學分支中取得了實質(zhì)性突破：
OEIS猜想：系統(tǒng)自動形式化了492個開放猜想，證明了其中44個。為防止形式化錯誤，系統(tǒng)要求先證明「測試引理」——驗證序列前幾項與形式化定義一致——才能嘗試目標猜想。
代數(shù)幾何：解決了一個懸置約15年的開放問題——證明了余維數(shù)3、類型2的純O-序列的對數(shù)凹性。這個問題此前被認為是該領(lǐng)域最后一個主要未解情況。
凸優(yōu)化：解決了一個關(guān)于錨定梯度下降-上升算法（Anchored GDA）精確收斂速率的開放問題。更妙的是，AI不僅驗證了一個固定算法，還在證明過程中自主搜索并發(fā)現(xiàn)了一個新的學習率調(diào)度參數(shù)，從而實現(xiàn)了更強的保證。
圖論：證明了Graffiti系統(tǒng)在1996年提出的一個關(guān)于生成樹葉子數(shù)與局部獨立集的猜想，形成了一個有趣的閉環(huán)——AI證明了另一個AI提出的猜想。
加法組合學：幫助解決了Ben Green著名開放問題列表中的第57題。
量子光學：與Mario Krenn合作，解決了多個關(guān)于單色量子圖的猜想，對應高維GHZ量子態(tài)的構(gòu)造。
三路合圍，數(shù)學前沿全面失守
2026年5月，AI在數(shù)學領(lǐng)域的造詣，幾乎同時達到了研究級水平。
OpenAI走的是自然語言路線。
通用推理模型直接輸出證明，推翻了Erd?s 80年單位距離猜想。證明極其精妙，但驗證它需要人類頂級專家逐行審查。
菲爾茲獎得主Gowers把未解問題扔給GPT-5.5 Pro，兩小時拿到博士論文級成果，全程數(shù)學貢獻為零。
DeepMind走的是形式化驗證路線。
AlphaProof Nexus讓AI用Lean語言寫證明代碼，編譯器自動檢查每一步推理。任何一步出現(xiàn)邏輯斷裂，編譯器直接報錯，證明被拒絕。
自然語言路線靈活，但可能有幻覺。形式化路線可靠，但目前局限于Lean數(shù)學庫成熟的領(lǐng)域。
而DeepMind的數(shù)學家合作者發(fā)現(xiàn)了一個意料之外的收獲——
即使智能體無法證明目標定理，它生成的證明嘗試也加深了他們對問題的理解。因為草稿是形式化的，專家可以直接聚焦于未解決的子目標，而不需要重新驗證整個論證鏈。
換句話說，AI不只是在解題，它正在改變數(shù)學家思考問題的方式。
如今，未來的圖景已經(jīng)浮現(xiàn)：
AI先用自然語言探索證明思路，再用形式化系統(tǒng)逐步固化和驗證。
人類數(shù)學家的角色，則從「親手推導」轉(zhuǎn)向「提出問題、審查方向、提煉洞見」。
有人說，我們正目睹數(shù)學奇點的早期火花。
幾百美元算力，幾十小時運行，56年懸案告破，編譯器給出鐵證。
保羅·埃爾德什生前留下了1217道數(shù)學難題，懸賞后人求解。
他大概從未想過，有一天來領(lǐng)賞的，不是人類。
參考資料：
https://x.com/prz_chojecki/status/2058435083741061359?s=20
https://arxiv.org/abs/2605.22763v1
編輯：摩西
特別聲明：以上內(nèi)容(如有圖片或視頻亦包括在內(nèi))為自媒體平臺“網(wǎng)易號”用戶上傳并發(fā)布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
