北京
12月01日，據機器之心報道，普林斯頓大學數學博士Boris Alexeev借助數學AI智能體Aristotle（由Harmonic開發），在數小時內獨立證明了Erd?s問題#124的弱化版本。該問題由著名數學家Paul Erd?s提出，自1984年發表在《算術雜志》上以來一直懸而未決，核心涉及整數冪集的完備序列。
此次突破的關鍵在于：原始問題在三篇早期論文中存在表述差異，其中兩篇遺漏了關鍵假設，導致所形成的弱化版本意外地可通過已知的Brown判別法直接解決。Aristotle通過自然語言界面理解問題描述，并自動生成可在Lean4中驗證的形式化證明，展現了高效的自動化推理能力。
著名數學家陶哲軒（Terence Tao）對此表示關注，并在討論中分享自動化研究經驗。作為2006年菲爾茲獎得主、UCLA講席教授，陶哲軒是當代最活躍且最具影響力的數學家之一——他不僅曾解決困擾學界80余年的Erd?s差異問題，近年來更積極推動AI與形式化證明在數學研究中的應用。他認為，數學未解決問題呈“長尾”分布，AI能幫助規模化攻克相對容易的問題，摘取“低垂的果實”。
陶哲軒去年運行Equational Theories項目時，使用自動化方法在幾天內解決了2200萬個蘊含式中的相當大部分。他建議研究者系統性地掃描剩余問題，尋找更多快速解決方法。
目前Erd?s問題網站收錄1108個問題，研究者正結合AI工具和形式化證明助手，集中清理底層問題。Aristotle智能體已在GitHub開源證明過程。
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
