30年數學難題，AI僅6小時告破！陶哲軒：ChatGPT們都失敗了
昨晚，數學界炸了！AI數學家「亞里士多德」竟在6個小時內，一鍵破解了30年難題的簡版，引陶哲軒盛讚。數學領域Vibe proving時代來了。
30年未解數學難題，終於告破！
由HarmonicMath開發的AI數學家「亞里士多德」（Aristotle），100%獨立完成了埃爾德什問題#124。
它在Lean證明系統中，耗時僅6個小時，驗證只需1分鐘。
全程沒有一絲人類的參与輔助，這一刻，堪稱數學界的「登月」時刻。
HarmonicMath創始人Vlad Tenev感慨道，「數學圈正迎來巨變，vibe證明的時代，來了」！
就連菲爾茲獎得主陶哲軒，高度讚揚了AI數學家「亞里士多德」。
AI發現數學的時代，正式開始了。
30年難題告破，AI做到了
一直以來，數學家Erdős Pál的「問題列表」，就像一座知識的珠穆朗瑪峰，考驗著人類的極限。
那些懸而未決的難題，懸賞金大多從幾十美元到上萬美元不等。
其象徵意義遠大於實際價值，成為了無數數學家的精神勳章。
30年來，第124號問題（Erdős #124）在論文「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
順便提一句，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正在點亮數學的「暗森林」。
正如陶哲軒所言，「自動化工具先清理掉最容易的問題，把真正難啃的那部分剝離出來，讓人類數學家把精力花費在值得的地方」。
*以上內容系網友澳洲一點通自行轉載自新智元，該文僅代表原作者觀點和態度。本站系信息發布平台，僅提供信息存儲空間服務，不代表贊同其觀點和對其真實性負責。如果對文章或圖片/視頻版權有異議，請郵件至我們反饋，平台將會及時處理。