12月01日，據(jù)機(jī)器之心報(bào)道，普林斯頓大學(xué)數(shù)學(xué)博士Boris Alexeev借助數(shù)學(xué)AI智能體Aristotle（由Harmonic開(kāi)發(fā)），在數(shù)小時(shí)內(nèi)獨(dú)立證明了Erd?s問(wèn)題#124的弱化版本。該問(wèn)題由著名數(shù)學(xué)家Paul Erd?s提出，自1984年發(fā)表在《算術(shù)雜志》上以來(lái)一直懸而未決，核心涉及整數(shù)冪集的完備序列。

此次突破的關(guān)鍵在于：原始問(wèn)題在三篇早期論文中存在表述差異，其中兩篇遺漏了關(guān)鍵假設(shè)，導(dǎo)致所形成的弱化版本意外地可通過(guò)已知的Brown判別法直接解決。Aristotle通過(guò)自然語(yǔ)言界面理解問(wèn)題描述，并自動(dòng)生成可在Lean4中驗(yàn)證的形式化證明，展現(xiàn)了高效的自動(dòng)化推理能力。

著名數(shù)學(xué)家陶哲軒（Terence Tao）對(duì)此表示關(guān)注，并在討論中分享自動(dòng)化研究經(jīng)驗(yàn)。作為2006年菲爾茲獎(jiǎng)得主、UCLA講席教授，陶哲軒是當(dāng)代最活躍且最具影響力的數(shù)學(xué)家之一——他不僅曾解決困擾學(xué)界80余年的Erd?s差異問(wèn)題，近年來(lái)更積極推動(dòng)AI與形式化證明在數(shù)學(xué)研究中的應(yīng)用。他認(rèn)為，數(shù)學(xué)未解決問(wèn)題呈“長(zhǎng)尾”分布，AI能幫助規(guī)模化攻克相對(duì)容易的問(wèn)題，摘取“低垂的果實(shí)”。

陶哲軒去年運(yùn)行Equational Theories項(xiàng)目時(shí)，使用自動(dòng)化方法在幾天內(nèi)解決了2200萬(wàn)個(gè)蘊(yùn)含式中的相當(dāng)大部分。他建議研究者系統(tǒng)性地掃描剩余問(wèn)題，尋找更多快速解決方法。

目前Erd?s問(wèn)題網(wǎng)站收錄1108個(gè)問(wèn)題，研究者正結(jié)合AI工具和形式化證明助手，集中清理底層問(wèn)題。Aristotle智能體已在GitHub開(kāi)源證明過(guò)程。