近日，券商巨頭 Robinhood 首席執行官弗拉德·特涅夫（Vlad Tenev）在社交媒體上發布了一條推文：“我們正處于數學領域深刻變革的風口浪尖。氛圍證明（Vibe proving）的時代已經到來。”

他宣布，自己創辦的人工智能公司 Harmonic 開發的 Aristotle 模型完全自主地解決了埃爾德什問題（Erd?s Problem）124 號，這個數論猜想自 1995 年在學術期刊《Acta Arithmetica》上首次提出以來，已經懸而未決近三十年。

圖丨相關推文（X）

不到 24 小時后，埃爾德什問題網站的維護者托馬斯·布魯姆（Thomas Bloom）也發表了一系列評論。“這是一個很好的證明，完全由人工智能從形式化陳述出發、無人工干預生成，然后在 Lean 中形式化，這本身已經令人印象深刻，”布魯姆寫道，“事后來看，解決方案相當簡單，使得這個問題處于數學競賽題的水平。埃爾德什提出這個問題時有兩個不同的版本。人工智能解決的是更簡單的那個。”

埃爾德什問題 124 號問的是：給定一組整數 d?, d?, ..., d?，如果它們滿足∑1/(d?-1)≥1，那么是否所有足夠大的整數都可以表示為一種特殊形式的和——每一項都是某個 d? 的冪次，且該冪次在 d?進制下只包含數字 0 和 1？在 1995 年的原始論文中，伯爾（Burr）、埃爾德什、格雷厄姆（Graham）和李文卿（Wen-Ching Li）明確排除了 1 的冪次，并附加了一個必要的最大公約數條件。但埃爾德什本人在后來的論文中重新表述這個問題時，卻允許包含 1，并省略了最大公約數條件。Aristotle 解決的是后者。

圖丨埃爾德什問題 124 號（Erd?s Problem）

“如果這樣的簡單方法有效，那么伯爾、埃爾德什、格雷厄姆和李這樣的聯合智慧肯定早就發現了，”布魯姆寫道。通常情況下，這會讓他懷疑證明中存在被忽視的微妙之處，但由于證明已經在 Lean 證明助手中形式化，也就是說每一步推理都經過了機器驗證，“顯然它確實有效！”

證明該問題的普林斯頓大學數學博士鮑里斯·阿列克謝耶夫（Boris Alexeev）在討論區詳細描述了 Aristotle 的工作過程。他使用的是一個測試版本，具有增強的推理能力和自然語言界面。Aristotle 花費了 6 小時生成證明，而 Lean 的類型檢查只用了 1 分鐘。

值得一提的是，Aristotle 完全是從形式化陳述出發工作的，期間沒有任何人工干預。只是阿列克謝耶夫發現并修正了形式化猜想項目中的一個打字錯誤——注釋寫的是“≥1”，而 Lean 代碼卻是“=1”。最終，Aristotle 證明了三個不同版本的問題。

Aristotle 的證明的確展現出一種令人意外的簡潔美。一位名為 tsaf 的用戶在討論區用幾行文字概述了核心思路：將所有 d? 的冪次按升序排列形成序列 (a?)。例如，如果 d?=2 且 d?=3，序列就是 1, 1, 2, 3, 4, 8, 9, 16, 27, ...。

證明的關鍵是表明 a???-1 ≤ a?+...+a?。如果這個不等式成立，那么通過歸納法，可以用前 n 項的子序列和來填“滿”從 1 到 a?+...+a? 的所有整數，而這個范圍恰好足以覆蓋 a???。

而關鍵就在于對 a?+...+a? 這個總和的處理。將它改寫為 ∑(d?^(e?,?)-1)/(d?-1)，其中 e?,? 是 d? 在前 n 項中尚未出現的第一個指數。根據構造，a??? 恰好等于 mini(d?^(e?,?))。由于問題假設 ∑1/(d?-1)≥1，而 d?^(e?,?)≥1，通過仔細計算就能驗證所需的不等式。整個論證就是這幾步推理，在 Lean 中的形式化證明也相對緊湊。

圖丨相關評論（Erd?s Problem）

特涅夫的導師、菲爾茲獎得主陶哲軒也在討論區出現了。他做了一個有趣的實驗：將這個問題（簡化版本）提供給谷歌的 Gemini Deepthink，并提示使用布朗準則（一個在加法組合學中常用的工具）。Gemini 宣稱布朗準則不太可能強大到足以解決這個問題。

檢查其推理過程后，陶哲軒發現這是一個“相當體面的錯誤”。Gemini 注意到，如果取 d?=3，在 3^k 和 3^(k+1) 之間可能無限次地不存在任何其他 d?的冪次，使得連續元素之間的比率可能高達 3。布朗準則通常需要連續元素的平均比率不超過 2，因此 Gemini 從啟發式角度認為這種方法不太可能奏效。

“這實際上不是一個糟糕的分析，”陶哲軒評論道，“只是恰好所有小于 3^k 的其他冪次的累積和（勉強）足以克服 3 的間隙并最終到達 3^(k+1)。我會將這類錯誤歸類為人類專家在這個問題上也可能犯的錯誤。”

他還指出，這種分析也暗示了為什么該問題的更強版本更加困難——在不允許 1 的情況下，序列的結構會發生根本變化，上述簡潔的論證將不再適用。

陶哲軒進一步用龐梅朗斯（Pomerance）的觀察來解釋問題的微妙之處：通過丟番圖逼近論可以證明，對于有限集合，條件 ∑1/(a-1)≥1 是必要的。但當這個和恰好等于 1 時，問題變得極其微妙，至少需要貝克定理（Baker's theorem）這樣的深刻結果來防止不同底數的冪次聚集得太近，從而產生潛在的反例。

薩格勒布大學理學院數學系教授韋科·科瓦奇（Vjeko Kovac）也提供了另一個視角。他指出，在他與陶哲軒此前發表的一篇論文中的定理 2.3 可以被視為這個問題的連續參數變體，基本證明思路（排序序列、驗證條件、考慮與每個參數相關的第一個出現項等）是相同的。

“我提到這一點并非要貶低 Aristotle 和阿列克謝耶夫的證明，恰恰相反，它非常漂亮，”科瓦奇寫道，“我的觀點是，基本思想在許多地方重復出現；人類常常未能意識到它們適用于不同的環境，而機器沒有這個問題！我記得以前見過這個問題并簡短地思考過它。我承認，我當時沒有注意到這個聯系，而現在對我來說卻相當明顯。”

科瓦奇的這段話也說明，Aristotle 找到的證明并非某種前所未有的創新技術，而是將已經存在于數學文獻中的基本思想應用到了這個具體問題上。陶哲軒的實驗進一步印證了這一點。

當他讓 ChatGPT Pro 處理同樣的問題時，該工具直接從埃爾德什問題網站上檢索到了 Aristotle 的證明和 tsaf 的總結，并將其改寫成人類可讀的形式。陶哲軒注意到，可能存在關閉網絡搜索的選項來測試工具獨立解決問題的能力，但他沒有探索這一點。

布魯姆也提出了類似的疑問。他表示不會感到驚訝如果這個已解決的問題實際上曾出現在某個數學競賽中，這樣它可能已經是訓練數據的一部分。在數學競賽中，參賽者通常被告知一個簡短優雅的解法是存在的——這正是 Aristotle 面對的情況。

問題在于，當四位數學家在 1995 年提出這個猜想時，他們并不知道是否存在這樣的簡單解法，而這種不確定性才是數學研究的常態。至于這個問題為何 30 年都沒被解決，大概只是因為沒有人真的認真嘗試去解決它。

圖丨Aristotle 的證明過程（Harmonic）

因此，就目前來看，Aristotle 確實能夠在形式化的框架內探索證明空間，找到滿足邏輯要求的推理鏈條。但這種能力更接近于在已知的數學工具箱中尋找合適的組合，而非發明全新的證明技術或提出原創的數學洞察。當基本思想已經在文獻的某個角落存在時，人工智能展現出了發現和應用它們的能力；但當需要真正的概念突破時，情況可能會大不相同。

布魯姆最終決定保持埃爾德什問題 124 號的“開放”狀態，在主要陳述中保留最大公約數條件，并在備注中說明簡化版本已被解決。阿列克謝耶夫對此表示同意：“Aristotle 解決了這個問題的‘一個’版本，但不是‘那個’版本。”這個微妙的區分，或許正是理解人工智能當前數學能力的關鍵。

參考資料：

1.https://x.com/vladtenev/status/1994922827208663383

2.https://x.com/thomasfbloom/status/1995094668879462466

3.https://www.erdosproblems.com/forum/thread/124

運營/排版：何晨龍