Google DeepMind 的數學證明系統 AlphaProof Nexus 正式刊登在 Science 上。論文第一作者署名為 Tsoukalas，研究團隊全部來自 DeepMind。這項研究 5 月底先以預印本公開，這次是經過同儕審查後的期刊版本。
成績單沒有改變：系統嘗試了 353 道尚未解決的 Erdős 問題，解出 9 道，其中 2 道已懸而未決 56 年；在整數數列資料庫 OEIS 的 492 個開放猜想中證出 44 個；此外還回答了代數幾何中一個關於 Hilbert 函數、懸置約 15 年的問題，並改進了 min-max 最佳化中的一個已知界。
一個 Gemini，一個 Lean 編譯器
系統的底層是 Gemini 3.1 Pro。模型以形式化語言 Lean 草擬證明，Lean 編譯器每改一步就檢查一次，錯誤訊息直接回饋給下一輪嘗試。整個過程中，人只在最後檢視結果。
論文拆出了四個版本：
- A 版：最樸素的「生成—驗證」迴圈，大型語言模型負責寫，編譯器負責判；
- B 版：在 A 的基礎上接入 DeepMind 先前的證明器 AlphaProof，專門補上證明中缺少的片段；
- C 版：加入演化機制，多個子代理共享一池證明草稿，並以 Elo 分數排序；
- D 版：以上全部疊加，用來攻克 Erdős 問題。
結果中最耐人尋味的一點，是 A 版也獨立證出了全部 9 道 Erdős 題，只是在最難的幾道上花費更多。The Decoder 引述的推論成本是每道題數百美元。作者在論文中的說法是：
"power of compiler feedback in grounding LLM reasoning"
（編譯器回饋能把大型語言模型的推理牢牢釘在實處。）
西班牙學者的幾處保留
西班牙科學媒體中心在論文上線當天，邀請幾位當地學者點評，意見分成兩派。
UAM 研究員 Pablo Haya Coll 認為，這套方法能系統性地產出有分量的數學發現。UOC 的 Josep Curto 給出的評價是 "a dazzling display of technical capability marred by significant methodological inconsistencies"，大意是技術上令人眼花撩亂，方法上卻有明顯的前後不一。他列出三點：A 版與 D 版解出同一批題目，顯示框架複雜度未必決定發現能力；成本只計算了成功的那些執行，B 版和 D 版的帳裡也沒有計入 AlphaProof 本身的推論開銷；Lean 只能保證證明對「寫下來的那條命題」成立，命題是否忠實翻譯了原題，仍須靠數學家人工核對，論文也承認出現過形式化錯誤。
ICMAT 所長 Javier Aramayona 擔心的是另一件事：大批「已知為真、卻沒有人完全讀懂」的結果開始出現，數學研究中理解的那一環，以及年輕研究者的訓練過程，都可能被削弱。巴亞多利德大學的 Teodoro Calonge 則說得更直接，這個領域還有相當大的改進空間。
作者自己也寫明了適用範圍：AI 在 Erdős 問題上的整體成功率大約為 1% 到 2%，解出的多是相對容易的題目，集中在組合學、凸最佳化和數論這些 Mathlib 函式庫累積較厚、問題容易拆成子目標的方向。需要發明大量新理論的問題，系統基本上碰不到。
把今年幾件事串起來看
5 月，本站曾報導 OpenAI 模型攻克一個有 80 年歷史的 Erdős 猜想；9 月，數學家與 OpenAI 之間又發生過一場署名之爭；10 月 6 日，OpenAI 在 GitHub 上一次釋出 722 篇 AI 生成的數學手稿，採用開源儲存庫加 Apache 2.0 授權的方式，沒有走期刊。The Decoder 的報導提到，由陶哲軒領頭的一個數學家團體隨後呼籲抵制這種做法。
兩家公司的路徑差異在這裡看得很清楚。OpenAI 選擇量大、公開，讓社群自己去篩選；DeepMind 選擇數量少得多，但每一條都通過了 Lean 編譯器，也通過了期刊審稿。後者在論文中對 Lean 的定位也相當節制，原話是形式化驗證 "can serve as a filter for determining which proofs merit human review"，也就是用來決定哪些證明值得人去看。
粗略算一下：以每題數百美元計，9 道 Erdős 題的推論開銷遠低於一位博士後研究員一個月的薪水；但依 Curto 指出的口徑，把失敗的執行和 AlphaProof 的呼叫加進來之後，帳面上會增加多少，論文目前並未給出數字。DeepMind 已把證明和部分說明放在 GitHub 的 alphaproof-nexus-results 儲存庫，外部數學家可以逐條核對。
參考來源：Science 期刊論文、The Decoder、CocoLoop、西班牙科學媒體中心專家點評；已核對論文正文中 353 道 Erdős 問題解出 9 道、492 個 OEIS 猜想證出 44 個，以及四個代理版本的分工。