近日，數學界傳來一則引人關注的消息：Erdos問題#124的一個弱化版本被成功證明。這一成果由普林斯頓大學數學博士Boris Alexeev完成，他借助Harmonic公司開發的數學AI智能體Aristotle，對問題展開了深入研究并取得突破。

Erdos問題#124的提出可追溯到1984年，當時在《算術雜志》發表的論文《整數冪集的完備序列》中首次提出該問題，此后近30年一直懸而未決，成為數學領域的一大難題。此次Boris Alexeev的證明，雖只是弱化版本，但仍引發了廣泛關注。不過，此前一些報道稱AI獨立解決了該問題的完整版本，這一說法并不準確，還引發了不少爭議，Boris Alexeev為此專門進行了修正說明。

在Formal Conjectures項目中，該猜想有正式聲明，但聲明中存在拼寫錯誤，注釋在顯示式方程里顯示為“≥1”，而相應的Lean聲明為“= 1”，這使得聲明變弱。Boris Alexeev對此進行了修正，并給出了修正后聲明的證明，還刪除了他認為不必要的聲明部分，而Aristotle也證明了這些刪除內容的正確性。有學者指出存在涉及冪次1（對應個位數）的問題，意味著[BEGL96]中的猜想與當前情況不同，Boris Alexeev認為[Er97]中的版本與當前陳述相符，不過目前他無法獲取[Er97e]來核實。

盡管此次證明存在一些微妙情況，Erdos問題#124目前仍是一個開放問題，但數學智能體獨立證明其較簡單版本，已然展現出強大的數學證明能力。Erdos問題#124的具體內容，可在其官方論壇查看相關鏈接。

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

在Erdos問題#124的討論中，有學者簡要介紹了Aristotle針對該問題的證明方法，稱其“出奇的簡單”。對詳細證明過程感興趣的讀者，可參考相關開源倉庫中的文件。

著名數學家陶哲軒對AI在數學領域的應用一直保持高度關注，在Erdos問題#124的討論中也能看到他的評論。陶哲軒認為，數學中的未解決問題如同許多真實世界中的分布一樣，呈現出典型的“長尾”結構。其中有很多相對容易、未得到足夠關注的問題，借助AI強大的自動化和推理能力，規模化地嘗試攻克這些問題，就能收獲許多“低垂的果實”。

陶哲軒在去年運行Equational Theories Project時就有過類似體驗。該項目針對普遍代數中的2200萬個蘊含式展開研究，利用簡單自動化方法的最初幾輪掃描，在幾天內就解決了相當大一部分問題；隨后采用越來越復雜的方法，逐步攻克早期掃描中頑固抵抗的剩余實例，最后少數幾個蘊含式則花費數月人類努力才解決。陶哲軒以個人日志形式完整記錄了該項目的詳細過程、方法、結果和個人思考。

Erdos問題網站的情況與之類似，目前收錄了1108個在至少一篇埃爾德什論文中提出過的問題，其中既有極其困難的經典難題，也有大量偏門、連Erdos本人都沒怎么關注過的問題。如今，陶哲軒開始采用自動化方法，集中清理這些“低垂果實”。幾周前，網站上一批原本標注為未解決的問題突然被劃為“已解決”，原因是AI驅動的文獻搜索工具發現解答早已存在于文獻中。研究這些問題的數學家們也結合使用AI工具和形式化證明助手，用Lean驗證已有證明、生成問題關聯的整數序列項或補全推理步驟。

具體到Erdos問題#124，該問題在三篇論文中被提出，但其中兩篇漏掉關鍵假設，導致問題在那兩種表述下成為已知結果（Brown判別法）的推論，這一點直到Boris Alexeev使用Aristotle工具處理問題時才被發現。Aristotle在數小時內就自主找到并用Lean形式化了該弱化版本的解答。目前，研究者正系統性掃描網站上剩余問題，尋找更多類似誤述或快速解決方法，短期內主要聚焦“長尾”末端。隨著自動化工具能力不斷增強，它們不僅能幫助人類數學家清除容易部分，還能讓真正困難的問題更加清晰地呈現出來。