人工智能幫助解決以前無(wú)法解決的數(shù)學(xué)問(wèn)題的案例越來(lái)越多。

據(jù)報(bào)道，OpenAI 的 GPT-5.2 解決了 Erd?s 問(wèn)題 #728，這似乎是一個(gè)重要的里程碑，標(biāo)志著人工智能首次在任何人類數(shù)學(xué)家之前自主解決了一個(gè)未解的數(shù)學(xué)猜想。

劍橋大學(xué)數(shù)學(xué)系學(xué)生 AcerFur 在 X 平臺(tái)上宣布了這項(xiàng)突破性進(jìn)展，此前他曾與他人合作進(jìn)行驗(yàn)證。該問(wèn)題旨在探究是否存在無(wú)窮多個(gè)整數(shù) a、b、n，滿足特定的整除性和涉及階乘的不等式條件。自提出以來(lái)，該問(wèn)題一直未得到解決。具體而言，該問(wèn)題是：“設(shè) C>0 且 ?>0 足夠小。是否存在無(wú)窮多個(gè)整數(shù) a、b、n，滿足 a≥?n 且 b≥?n，使得 a!b!∣n!(a+b?n)! 且 a+b>n+Clogn？”

根據(jù) AcerFur 的描述，GPT-5.2 生成了初始解決方案和證明，隨后 Harmonic 的 Aristotle 系統(tǒng)使用 Lean 中的形式化驗(yàn)證對(duì)其進(jìn)行了驗(yàn)證。Lean 是一款證明輔助工具，可提供機(jī)器可驗(yàn)證的正確性保證。Aristotle 最初解決了一個(gè)稍弱的變體，但能夠自主修復(fù)其證明，最終無(wú)需人工干預(yù)即可獲得完整的結(jié)果。

重要注意事項(xiàng)

AcerFur強(qiáng)調(diào)了這項(xiàng)成就的三個(gè)關(guān)鍵缺陷。首先，原始問(wèn)題描述含糊不清，該模型求解的是一種數(shù)學(xué)界普遍認(rèn)為最有可能產(chǎn)生非平凡解的解釋。其次，該解決方案似乎深受數(shù)學(xué)家Carl Pomerance先前工作的啟發(fā)，這引發(fā)了人們對(duì)人工智能貢獻(xiàn)究竟有多新穎的質(zhì)疑。第三，目前尚不清楚有多少尚未發(fā)表的文獻(xiàn)探討了如何解決此類問(wèn)題的特殊情況。

該解決方案源于 AcerFur 和 X 用戶 Liam06972452 的合作。Liam06972452 首先收到了 GPT-5.2 的響應(yīng)并請(qǐng)求驗(yàn)證。AcerFur 解釋說(shuō)，GPT-5.2 完成了繁重的數(shù)學(xué)運(yùn)算，而 GPT-5.2 Pro 則隨后將證明結(jié)果格式化為完整的 LaTeX 論文格式，并在格式化過(guò)程中可能進(jìn)行了驗(yàn)證并填補(bǔ)了其中的空白。

人工智能數(shù)學(xué)領(lǐng)域的發(fā)展勢(shì)頭

這項(xiàng)成就緊隨Harmonic公司近期另一項(xiàng)成果之后。Harmonic是一家數(shù)學(xué)人工智能初創(chuàng)公司，由Robinhood首席執(zhí)行官Vlad Tenev創(chuàng)立。去年11月，Harmonic宣布其亞里士多德系統(tǒng)解決了埃爾德什問(wèn)題124，該問(wèn)題自1995年發(fā)表以來(lái)，已懸而未決近30年。

然而，數(shù)學(xué)界對(duì)這一說(shuō)法反應(yīng)較為謹(jǐn)慎。維護(hù)埃爾德什問(wèn)題網(wǎng)站的托馬斯·布魯姆承認(rèn)這一成就令人印象深刻，但他指出，所解決的版本只是埃爾德什提出的兩個(gè)變體中較簡(jiǎn)單的一個(gè)，而且事后看來(lái)，解決方案相對(duì)簡(jiǎn)單直接，難度與人工智能已展現(xiàn)出強(qiáng)大實(shí)力的數(shù)學(xué)競(jìng)賽題目相當(dāng)。

埃爾德什問(wèn)題指的是保羅·埃爾德什提出的數(shù)學(xué)猜想。埃爾德什是20世紀(jì)最多產(chǎn)的數(shù)學(xué)家之一，一生發(fā)表了1500多篇論文。解決埃爾德什問(wèn)題被認(rèn)為是數(shù)學(xué)界的一項(xiàng)重大成就，埃爾德什本人也根據(jù)他對(duì)問(wèn)題難度的評(píng)估，為解答者提供獎(jiǎng)金。

形式化驗(yàn)證的優(yōu)勢(shì)

這兩項(xiàng)成果都凸顯了形式化驗(yàn)證在驗(yàn)證人工智能生成的數(shù)學(xué)運(yùn)算結(jié)果方面的重要性。Harmonic 的方法以 Lean 為核心，Lean 是一種形式化語(yǔ)言，它允許對(duì)每個(gè)解決方案進(jìn)行驗(yàn)證，直至其基本公理，從而無(wú)需人工數(shù)學(xué)家手動(dòng)檢查輸出結(jié)果的準(zhǔn)確性。

2025年初，Harmonic宣布其模型Aristotle在2025年國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽中取得了金牌級(jí)別的成績(jī)，在六道題目中給出了五道可驗(yàn)證的正確答案。這使得Harmonic與谷歌DeepMind和OpenAI等科技巨頭并駕齊驅(qū)，這兩家公司也分別憑借各自的模型取得了類似的成績(jī)。

啟示與問(wèn)題

如果這些論斷得到更廣泛的數(shù)學(xué)界的驗(yàn)證，它們可能標(biāo)志著人工智能系統(tǒng)發(fā)展的一個(gè)轉(zhuǎn)折點(diǎn)，人工智能系統(tǒng)將不再僅僅滿足于掌握現(xiàn)有的問(wèn)題集，而是開始貢獻(xiàn)原創(chuàng)性的數(shù)學(xué)發(fā)現(xiàn)。然而，關(guān)于這些解決方案的真正創(chuàng)新性、它們?cè)诙啻蟪潭壬鲜艿接?xùn)練數(shù)據(jù)的影響，以及它們究竟代表了真正的數(shù)學(xué)洞察力還是復(fù)雜的模式匹配，仍然存在諸多疑問(wèn)。

第 728 題最初表述的模糊性，以及 GPT-5.2 的解決方案大量借鑒了前人研究成果這一事實(shí)，凸顯了評(píng)估人工智能對(duì)數(shù)學(xué)貢獻(xiàn)的復(fù)雜性。盡管這些系統(tǒng)展現(xiàn)出了令人矚目的能力，但它們究竟是在進(jìn)行全新的研究，還是僅僅以新的方式重組了現(xiàn)有知識(shí)，仍然是一個(gè)值得探討的問(wèn)題?？梢钥隙ǖ氖?，人工智能系統(tǒng)正在迅速接近，甚至可能已經(jīng)達(dá)到了對(duì)數(shù)學(xué)研究做出有意義貢獻(xiàn)的門檻。這是否標(biāo)志著人工智能與人類在數(shù)學(xué)領(lǐng)域合作的新時(shí)代——或者更具變革性——還有待觀察。

閱讀最新前沿科技趨勢(shì)報(bào)告，請(qǐng)?jiān)L問(wèn)歐米伽研究所的“未來(lái)知識(shí)庫(kù)”

https://wx.zsxq.com/group/454854145828

未來(lái)知識(shí)庫(kù)是“ 歐米伽 未來(lái)研究所”建立的在線知識(shí)庫(kù)平臺(tái)，收藏的資料范圍包括人工智能、腦科學(xué)、互聯(lián)網(wǎng)、超級(jí)智能，數(shù)智大腦、能源、軍事、經(jīng)濟(jì)、人類風(fēng)險(xiǎn)等等領(lǐng)域的前沿進(jìn)展與未來(lái)趨勢(shì)。目前擁有超過(guò)8000篇重要資料。每周更新不少于100篇世界范圍最新研究資料。 歡迎掃描二維碼或訪問(wèn)https://wx.zsxq.com/group/454854145828進(jìn)入。