DeepMind 釋出 AlphaProof Nexus：用幾百美元算力，解開 56 年未解數學題

過去解決一個半個世紀沒人解開的數學難題，往往需要頂尖數學家閉關數年，甚至耗盡整個學術生涯。

現在，這個週期被壓縮成了幾個小時，外加一張幾百美元的算力賬單。

Google DeepMind 正式釋出 AlphaProof Nexus 論文。這個專門用於生成機器驗證數學證明的 AI 系統，在一共 353 個開放數學難題中，一口氣自主攻克了 9 個保羅·埃爾德什（Paul Erdős）難題，順便還證明了《整數序列線上百科全書》（OEIS）中的 44 個未解猜想。

這 9 個關於組合數學和圖論的難題裡，有兩個從 1970 年提出至今，已經整整 56 年無人能解。

把大模型和 Lean 焊死在一起

AlphaProof Nexus 的厲害之處，不在於它算得有多快，而在於它徹底擺脫了大模型容易「胡說八道」的毛病。

DeepMind 把大語言模型和一個叫做 Lean 的形式化證明輔助工具綁在了一起。大模型負責天馬行空地給出證明思路和步驟，Lean 則扮演毫無感情的嚴苛裁判。

系統把步驟翻譯成程式碼扔給 Lean，Lean 負責跑編譯器級別的形式化驗證。只要有一步邏輯不嚴密，直接打回重來；大模型根據反饋重新調整，不斷迴圈，直到 Lean 判定完全通過。

完整版的 Agent 裡甚至加入了進化演算法，用來最佳化求解路徑。DeepMind 也測試過一個更簡化的版本，雖然最終也能解出同樣的結果，但算力消耗和花費明顯高得多。

這也把前沿數學研究的門檻拉到了一個誇張的地步：解開一個半個世紀的難題，單題推理成本只要幾百美元。

剛被 OpenAI 搶了風頭，隔天就反擊

有意思的是這次釋出的時機。

就在論文公開的前一天，OpenAI 剛剛宣佈自己的 AI 推翻了一個存在 80 年的埃爾德什猜想。而在此幾個月前，OpenAI 還曾因為宣稱攻克 10 個新難題不嚴謹而被迫撤回過說法。

OpenAI 剛找回場子，DeepMind 隔天就甩出了一份更重磅的戰報，而且拿出的是經受過機器形式化驗證的硬核證明。

不過 AlphaProof Nexus 也不是萬能的。論文坦承，那些需要憑空發明全新數學工具或全新構造的難題，目前的 AI 依然完全無能為力。

為什麼重要

我們認為，AlphaProof Nexus 最大的意義，是證明了 AI 正在從「做題家」變成「研究員」。

以前大模型刷各種奧數競賽題，本質上還是在人類畫好的靶子內部打轉。但面對 50 多年沒人見過正確答案的開放數學猜想，AI 給出了真正的原始突破。

對數學界來說，這種工具不會砸掉數學家的飯碗，反而會成為極其強悍的研究副駕駛。人類學者負責提出宏觀猜想和方向，繁瑣、漫長、極度消耗腦力的構造與驗證過程，完全可以打包丟給幾百美元算力的 AI 去掃雷。

對行業而言，這場競爭也標誌著 AI 推理的評測基準徹底換代。當模型在公開基準上全員拿滿分時，去未解科學前沿實測，就成了巨頭之間唯一有說服力的試金石。

DeepMind 這一步走得相當漂亮。它用 Lean 形成閉環，用確定性幹掉了不確定性。雖然它現在還不能像大師那樣開創全新的數學流派，但把已知世界的邏輯推演做到極致，本身就已經足夠改變遊戲規則了。