AI獨立解決三十年數學問題的變體，陶哲軒分享自動化研究經驗

機器之心報道

機器之心編輯部

剛剛，Erdos 問題 #124 的一個弱化版本被證明。

這個問題自 1984 年在《算術雜志》上發表的論文 「整數冪集的完備序列」 中提出以來，近 30 年一直懸而未決

證明該問題的是普林斯頓大學數學博士 Boris Alexeev ，使用了來自 Harmonic 的數學 AI 智能體 Aristotle運行了這個問題，智能體最近更新了更強的推理能力和自然語言界面。

關于該問題的一些報道都聲稱AI獨立解決了該問題的完整版本，事實卻并非如此，產生了很多爭議。Boris Alexeev 為此進行了修正：

在 Formal Conjectures 項目中，該猜想有一個正式聲明。不幸的是，該聲明中有一個拼寫錯誤，其中注釋在顯示式方程中顯示為 「≥1」 ，而相應的 Lean 聲明為 「= 1」。（這使得聲明變弱了。）因此，我也修正了這個問題，并包含了對修正后聲明的證明。最后，我刪除了我認為是不必要的聲明方面，Aristotle 也證明了這一點。
正如 DesmondWeisenberg 所提到的，存在一個涉及冪次 1（這里對應個位數）的問題，這意味著 [BEGL96] 中的猜想與此不同。我相信 [Er97] 中的版本與這里的陳述相符，部分原因在于它缺少 [BEGL96] 中明顯必要的最大公約數條件。我目前無法獲取 [Er97e] 來檢查其中的陳述。考慮到Aristotle 的成就，這個問題如此微妙，實在不幸！

盡管如此，數學智能體獨立地證明了 Erdos 問題#124的較簡單版本，仍然表現了令人驚訝的數學證明能力。

Erdos 問題 #124 內容如下圖所示，由于該證明存在微妙的錯誤，目前仍是一個開放問題。

• Erdos 問題 #124 鏈接：https://www.erdosproblems.com/forum/thread/124

數學 AI 智能體 Aristotle 是一個一個用于自動形式化和形式驗證的 API。根據 Harmonic 的介紹，其具備利用 IMO 金牌級引擎解決最復雜的推理問題的能力；可以自動將英語陳述和證明轉換為經過驗證的 Lean4 證明；能夠無縫集成到項目中，自動利用用戶的整個定理庫和定義、依賴項以及 Mathlib。

• Aristotle 鏈接：https://aristotle.harmonic.fun/

在 Erdos 問題 #124 的討論中，tsaf 簡要介紹了 Aristotle 針對該問題的證明方法，稱其「出奇的簡單」

有關詳細的證明過程，感興趣的讀者可以參考：

• https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124.md

對于 AI 獨立進行完整的數學難題的證明，陶哲軒進行了深度的關注。在該問題下，也能看到他的評論。

陶哲軒對于 AI 工具在數學領域的觀點仍然一以貫之，他認為像許多其他真實世界中的分布一樣，數學中的未解決問題也呈現出典型的「長尾」結構

在數學的未解決問題中有很多沒有得到關注的相對容易的問題，借助人工智能的強大自動化能力和推理能力去規模化地嘗試攻克這些問題，就會有許多「低垂的果實」唾手可得。

陶哲軒在去年運行 Equational Theories Project 時親眼見證了這一點。

這個項目攻擊了普遍代數中 2200 萬個蘊含式。利用簡單的自動化方法的最初幾輪掃描，在幾天內就解決了其中相當大的一部分；隨后又使用越來越復雜的方法，逐步攻克那些在早期掃描中頑固抵抗的剩余實例。最后的少數幾個蘊含式則花費了數月的人類努力才最終解決。

陶哲軒在這個項目中取得了大規模自動化數學研究的寶貴經驗，他以個人日志的形式完整記錄了研究的詳細過程，方法，結果和個人的思考。

• 日志鏈接：https://github.com/teorth/equational_theories/wiki/Terence-Tao's-personal-log

Erdos 問題網站也是類似的例子。該網站目前收錄了 1108 個在至少一篇埃爾德什論文中提出過的問題；其中當然包含一些極其困難的經典難題，但也有大量更偏門的問題，甚至連 Erdos 本人都沒怎么關注過。

與 Equational Theories 的經驗類似，陶哲軒現在也開始采用自動化方法，集中清理掉最底層的「低垂果實」。

幾周前，網站上一批仍被標注為未解決的問題突然被劃為「已解決」：AI 驅動的文獻搜索工具發現，它們的解答其實早已存在于文獻中。正在研究這些問題的數學家們也結合使用 AI 工具和形式化證明助手，來用 Lean 驗證已有證明、生成這些問題關聯的整數序列項，或補全某些方案中缺失的推理步驟。

陶哲軒認為，Erdos 問題#124的證明屬于另一類「低垂果實」，是由于描述中的技術性疏漏，而變得意外容易解決的問題。

具體來說，Erdos 問題 #124 在三篇論文中被提出過，但其中兩篇漏掉了一個關鍵假設，導致問題在那兩種表述下直接成為一個已知結果（Brown 判別法）的推論。然而，這一點直到 Boris Alexeev 使用 Aristotle 工具處理該問題時才被發現。Aristotle 在數小時內就自主找到并（用 Lean）形式化了該弱化版本的解答。

目前，研究者正系統性地掃描網站上的剩余問題，以尋找更多類似的誤述或快速的解決方法。這些努力短期內仍主要集中在「長尾」的最末端。

然而，這已經顯示出自動化工具能力的不斷增強，并在另一層面上幫助了研究這些問題的人類數學家：通過清除最容易的部分，使真正困難的問題更加清晰地呈現出來。

或許，從 AI 能夠獨立解決數學問題開始，我們就已站在數學領域深刻變革的邊緣。

數學領域 Vibe 證明的時代已經悄然而至。