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