6小時告破30年數學難題，亞里士多德一夜成名

30年懸而未決的數學難題就這樣被AI證明了？！

此時此刻，（前推特）正在刮起一股討論之風——

來自Harmonic的數學AI模型獨立證明了Erd?s問題#124，而這個問題已經被數學家無奈擱置了近30年。

微軟前AI副總裁、目前在OpenAI研究AGI的Sebastien Bubeck激動分享了這一消息，并表示：

• 該解決方案100%由AI生成，總計耗時6小時。

甚至連陶哲軒這樣的頂尖數學家也跑來圍觀討論，他在對比了Gemini和ChatGPT的深度研究工具后發現，Harmonic模型對該問題的證明表現更佳。

所以這到底是一個怎樣的問題？Harmonic模型又是如何“大顯神功”？

咱接著瞧——

AI證明了Erd?s問題#124簡易版

首先需要提醒，在聽完各路大神討論后，我們才意識到——

原來Harmonic模型所證明的并非原版Erd?s問題#124，而是一個簡易版本。

Erd?s問題#124需要提供的證明如下：

通俗理解即為：

假設你有k個不同的“進制生成器”，分別對應數字d1, d2, …, dk。

游戲規則為：1）你可以從每個生成器產生的數字列表中，至多挑選一個；2）然后把你挑出來的所有這些數字加起來；3）最后看能不能正好湊出你的目標數。

這個問題的核心就是——

只要你的這套“進制生成器”滿足一個特定的條件，即1/(d1-1) +1/(d2-1)+…+1/(dk-1)≥ 1，那么是不是所有的、足夠大的整數，都能用這種規則湊出來？

截至目前，這個問題取得的進展可以概括為：

就是說，這個問題在幾十年里逐漸演變為難易兩個版本。

在原版[BEGL96]中，挑戰者不允許使用數字1且需要額外滿足gcd條件（各個進制之間沒有“重復周期”），最終僅發現，對于特定集合 {3, 4, 7}猜想成立。

而當條件放寬之后（允許使用數字1且不需要額外滿足gcd條件），Harmonic模型成功證明只要滿足上述特定條件，就一定能湊出所有大整數，而且相關證明已經得到Lean形式化驗證。

Harmonic模型的證明方案如下，大佬們紛紛表示，這個方案出乎意料的簡單。

不過，此次用Harmonic模型證明#124簡易版的Boris Alexeev也補充道：

• 在“形式化猜想”項目中，原本有這個猜想的正式數學表述。但里面有個筆誤：注釋里寫的是≥1，而對應的Lean程序代碼里寫的卻是=1。這個錯誤讓原表述的條件變弱了，即只覆蓋了等于1的情況，而漏掉了大于1的情況。
• 因此，我修正了這個錯誤，并刪除了原表述中我認為不必要的部分。最終，AI成功證明了這個更簡潔、更準確的版本。

總結起來就是，Harmonic證明了問題#124的簡易版本，而困難版本仍懸而未決。

“Vibe證明時代已經到來”

盡管如此，大佬們還是對AI模型證明數學難題的潛力紛紛給予了肯定。

而參考編程領域的Vibe Coding概念（最早由AI大神卡帕西提出），Harmonic聯創兼CEO激動表示：

• 我們正處于數學領域深刻變革的邊緣，Vibe證明時代已經到來。

順著他的發言，我們也去扒了扒Harmonic模型背后的出品方，畢竟在陶哲軒眼中它這次可是戰勝了ChatGPT和Gemini。

根據公開資料，其背后公司名為Harmonic，目標也相當明確：

• 打造世界上最先進的數學推理引擎。

兩位聯創分別為Tudor Achim和Vlad Tenev。

CEO Tudor Achim，擁有卡內基梅隆大學計算機科學學士學位，同時也在斯坦福大學攻讀計算機科學PhD，不過現處于“on leave”狀態。

2023年，他和Vlad Tenev共同創辦了Harmonic，當時想打造世界上最先進的推理引擎。

更早之前，他還在一家自動駕駛輔助系統開發公司（Helm.ai）擔任聯創和CTO。

執行主席Vlad Tenev，擁有斯坦福大學數學學士學位和加州大學洛杉磯分校數學碩士學位。

除了在Harmonic擔任聯創和執行主席，他目前還同時在金融公司Robinhood Markets兼任CEO。

根據官網公開資料，Harmonic在大約一周前完成了1.2億美元（約合人民幣8.5億）C輪融資。

本輪融資由Ribbit Capital領投，估值達到14.5億美元（約合人民幣103億）。

Harmonic的旗艦模型就是本次用到的Aristotle模型（也有叫“亞里士多德”的），據悉它是第一個在2025年國際數學奧林匹克競賽中給出其中五道題形式化驗證解決方案的模型。

• Aristotle在保證準確性和消除幻覺的同時，達到了金牌級別的表現。

據Vlad Tenev透露，這次用的Aristotle進行了一些更新，具有更強大的推理能力和自然語言界面。

可以預見，隨著AI解決復雜數學問題的能力不斷突破，越來越多曾被“束之高閣”的百年難題將重見天日，并有望被逐一攻克。

Anyway，AI浪潮之下，開弓已無回頭箭。