新智元報道

編輯：桃子

昨晚，數學界炸了！AI數學家「亞里士多德」竟在6個小時內，一鍵破解了30年難題的簡版，引陶哲軒盛贊。數學領域Vibe proving時代來了。

30年未解數學難題，終于告破！

由HarmonicMath開發的AI數學家「亞里士多德」（Aristotle），100%獨立完成了埃爾德什問題。

它在Lean證明系統中，耗時僅6個小時，驗證只需1分鐘。

全程沒有一絲人類的參與輔助，這一刻，堪稱數學界的「登月」時刻。

HarmonicMath創始人Vlad Tenev感慨道，「數學圈正迎來巨變，vibe證明的時代，來了」！

就連菲爾茲獎得主陶哲軒，高度贊揚了AI數學家「亞里士多德」。

AI發現數學的時代，正式開始了。

30年難題告破，AI做到了

一直以來，數學家Erd?s Pál的「問題列表」，就像一座知識的珠穆朗瑪峰，考驗著人類的極限。

那些懸而未決的難題，懸賞金大多從幾十美元到上萬美元不等。

其象征意義遠大于實際價值，成為了無數數學家的精神勛章。

30年來，第124號問題（Erd?s ）在論文「Complete sequences of sets of integer powers」中提出后，至今無人破解。

E124核心是：給定k個自然數d_i ≥ 2，如果∑ 1/(d_i - 1) ≥ 1，那么對于自然數n，總存在a_i，使得n = ∑ a_i。

且每個a_i，在d_i下的「數字」僅限于{0,1}。

直白講，它本質上在問——極端約束下，是否總能用「二進制」表示任意大數，而不受基數干擾？

這牽扯到了「組合數學」的深水區，傳統方法卡在了gcd條件和邊界案例上。

直到昨晚，這堵墻崩塌了。

Harmonic團隊量身打造了「數學超級智能」原型——亞里士多德（Aristotle），結合了強化學習、蒙特卡洛樹搜索，以及Lean形式化語言。

輸入問題后，它通過搜索上億種證明策略，最終輸出了100%可驗證的定理。

數學家Boris Alexeev表示，這是AI輸出的三個定理中，自己最喜歡的一個：

theorem erdos_124 : ? k, ? d : Fin k → ?, (? i, 2 ≤ d i) → 1 ≤ ∑ i : Fin k, (1 : ?) / (d i - 1) → ? n, ? a : Fin k → ?, ? i, ((d i).digits (a i)).toFinset ? {0, 1} ∧ n = ∑ i, a i

地址：https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124.md

順便提一句，E124問題一共有兩個不同版本，全部由埃爾德什提出。

目前，AI亞里士多德解決的是一個比較簡單的版本。

在時間方面，Aristotle花了6小時，而Lean只花了1分鐘。

Erd?s問題的網站維護者表示，Aristotle的表現最令人深刻！

ChatGPT、Gemini都失敗了

陶哲軒對此點評道，就我所知，Gemini和ChatGPT的深度研究工具，都沒有找到關于這個問題的任何新的、有價值的文獻。

Gemini給出了一個簡單的觀察：如果把數字1排除掉，那么gcd條件就會變成必要的；它還解釋了條件

的重要性，并把它和一些關于Cantor集的平行研究聯系了起來，尤其是「Newhouse gap lemma」。

不過，它沒有找到與這個問題直接相關的新文獻。

ChatGPT則大量依賴本網頁作為主要權威來源，例如引用Aristotle的證明、本頁引用的其他論文，以及相關問題的頁面。

因此，并沒有獲得新的信息，不過讀者可能會覺得這些AI生成的總結還是挺有意思的。

陶哲軒：數學低垂果實，正被AI收割

在mathstodon上，陶哲軒還分享了多年來自己的經驗——

他表示，當前真實情況是：數學未解問題服從「長尾分布」，AI自動化「收割」恰恰集中在長尾最末端。

有大量問題其實相對容易證明或證偽，但因為真正能投入研究的專家數學家數量有限，這些問題幾乎沒得到過多少關注。

換句話說，這條「尾巴」里其實藏著不少觸手可及的「低垂果實」：

如果有辦法把這些問題進行大規模的自動化攻克，就可能產出相當多新的數學結果。

去年，陶哲軒在Equational Theories Project里親歷過一個類似的情況。

在這個項目中，他們面對的是普遍代數里2200萬條可能的蘊涵關系（implication），如果全靠人類去做，必定花費非常多的時間。

于是，他們決定從一開始用比較「低技術含量」的自動化方法，短短幾天就解決了大部分。

接下來，又不斷上復雜手段，啃那些前幾輪怎么都啃不動的頑固難點。

最后，剩下幾條特別頑固的，又花費了人類數學家幾個月的時間搞定。

目前，Erd?s問題網站收錄了1108個，曾在Erd?s至少一篇論文中出現過的問題。

其中，既有像E3這種臭名昭著的難題，也有數量眾多、更不起眼、幾乎沒人關注過的問題，甚至連Erd?s本人都沒再回頭研究過。

最近幾周，這個網站的「未解」標簽突然少了近十個，全部在AI加持下文獻搜索發現——

實際上，這些問題早就被他人解決。

正在研究這些問題的人類數學家也結合使用了AI工具和形式化證明助手：

有的在Lean里驗證已有證明，有的生成和這些問題相關的整數序列項，還有的補上某個既有思路里缺失的證明步驟。

最近，又發現了另一類落入自動化工具能力范圍的「低垂果實」——那些因為描述上存在技術性瑕疵而意外變得好解決的問題。

E124就是一個典型，這個問題完整版本有些難度，曾在Erd?s的三篇論文中出現。

但其中有兩篇遺漏了一個關鍵假設，使得這一版本其實只是Brown判據的直接推論。

這事一直沒有人發現，直到Boris Alexeev把問題丟給自動化工具Aristotle，沒想到AI在幾小時內自主找到了漏洞，并用Lean完成了形式化證明。

可以看到，AI正在點亮數學的「暗森林」。

正如陶哲軒所言，「自動化工具先清理掉最容易的問題，把真正難啃的那部分剝離出來，讓人類數學家把精力花費在值得的地方」。

參考資料：

https://www.erdosproblems.com/forum/thread/124-1892

https://x.com/SebastienBubeck/status/1994946303546331508?s=20

https://mathstodon.xyz/@tao/115639983683442577

https://x.com/thomasfbloom/status/1995094668879462466?s=20

秒追ASI

?點贊、轉發、在看一鍵三連?

點亮星標，鎖定新智元極速推送！