機器之心報道

機器之心編輯部

剛剛，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的證明屬于另一類「低垂果實」，是由于描述中的技術性疏漏，而變得意外容易解決的問題。

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

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

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

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

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