編輯推薦：
人工智能在數(shù)學(xué)領(lǐng)域的應(yīng)用取得顯著進(jìn)展，從ChatGPT的早期算術(shù)缺陷到大型語言模型如o4-mini在競賽中的優(yōu)異表現(xiàn)。數(shù)學(xué)家開始利用AI進(jìn)行探索性研究，如DeepMind與Williamson的協(xié)作項(xiàng)目，通過神經(jīng)網(wǎng)絡(luò)揭示復(fù)雜數(shù)學(xué)結(jié)構(gòu)中的隱藏規(guī)律。同時(shí)，符號AI工具如Lean被用于形式化證明，推動數(shù)學(xué)知識的大規(guī)模數(shù)字化（如Mathlib和ETP項(xiàng)目）。盡管AI展現(xiàn)出輔助研究潛力，但數(shù)學(xué)家仍對AI取代核心創(chuàng)造性工作存在擔(dān)憂，并強(qiáng)調(diào)需通過嚴(yán)格基準(zhǔn)測試和合作機(jī)制保障學(xué)科發(fā)展。
2022年秋季，隨著ChatGPT的問世，人工智能（AI）開始進(jìn)入公眾的視野。盡管ChatGPT在語法處理方面表現(xiàn)出色，但其數(shù)學(xué)能力卻相當(dāng)糟糕。當(dāng)被要求進(jìn)行簡單的數(shù)學(xué)運(yùn)算（比如加法）時(shí)，它可能會給出一串?dāng)?shù)字，其中開頭和結(jié)尾的數(shù)字是正確的，而中間的數(shù)字則是隨機(jī)生成的。這顯然表明：AI目前還無法勝任數(shù)學(xué)計(jì)算任務(wù)。
快進(jìn)到2025年，ChatGPT不僅在算術(shù)能力上有了顯著提升，而且那些具備更強(qiáng)推理能力的大型語言模型（LLMs）也開始在學(xué)校的數(shù)學(xué)作業(yè)中表現(xiàn)出色，并在數(shù)學(xué)競賽中獲獎(jiǎng)。
不過，AI在數(shù)學(xué)領(lǐng)域真正取得的進(jìn)步體現(xiàn)在數(shù)學(xué)家們開始將其應(yīng)用于研究之中。數(shù)學(xué)是一門歷史悠久的學(xué)科，而AI則是新興技術(shù)，但兩者之間存在著深厚的契合度。AI公司意識到了這一點(diǎn)，并開始與數(shù)學(xué)家們合作——許多數(shù)學(xué)家此前與任何形式的技術(shù)都幾乎毫無交集。
卡內(nèi)基梅隆大學(xué)哲學(xué)與數(shù)學(xué)科學(xué)教授、霍斯金森形式數(shù)學(xué)中心主任杰里米·阿維加德（Jeremy Avigad）表示，數(shù)學(xué)家們對AI充滿興趣和好奇。同時(shí)他也提到：“人們對AI如何改變數(shù)學(xué)領(lǐng)域，甚至可能取代某些被視為數(shù)學(xué)核心的概念感到擔(dān)憂。數(shù)學(xué)界仍在努力理解這項(xiàng)技術(shù)，并決定如何利用它。”
數(shù)學(xué)的研究方式
數(shù)學(xué)家們通過研究抽象對象和結(jié)構(gòu)，尋找其中的顯著特征（如形式、模式和對稱性）來進(jìn)行工作。他們會通過舉例分析、繪制圖表以及進(jìn)行計(jì)算來探索各種可能性，這一過程在很大程度上依賴于直覺。
然而，一旦數(shù)學(xué)家們?nèi)〉眯碌陌l(fā)現(xiàn)（即提出一個(gè)新的定理），接下來就需要撰寫嚴(yán)密的證明。雖然證明是用自然語言撰寫的，但其整個(gè)推理過程原則上都可以被嚴(yán)格驗(yàn)證，直至最基礎(chǔ)的邏輯層面。
數(shù)學(xué)研究的探索性和嚴(yán)謹(jǐn)性在兩種類型的AI中都有體現(xiàn)：一種是基于神經(jīng)網(wǎng)絡(luò)的AI（如機(jī)器學(xué)習(xí)），它通過處理大量數(shù)據(jù)來發(fā)現(xiàn)隱藏的模式和規(guī)律；另一種是基于符號系統(tǒng)的AI（如形式化證明助手），它通過邏輯推導(dǎo)得出精確的結(jié)論。
阿維加德指出：“AI在數(shù)學(xué)領(lǐng)域的魅力在于它結(jié)合了機(jī)器學(xué)習(xí)和符號方法的優(yōu)勢。如果能夠?qū)⑦@兩種技術(shù)融合在一起，就能實(shí)現(xiàn)兩全其美的效果：系統(tǒng)既能具備處理復(fù)雜問題的經(jīng)驗(yàn)和直覺，又能提供正確的證明和解釋。”
神經(jīng)網(wǎng)絡(luò)AI帶來的直覺
在探索階段，數(shù)學(xué)家們通常使用黑板、筆和紙進(jìn)行工作，有時(shí)也會借助計(jì)算機(jī)代數(shù)或圖形軟件輔助。不過近年來，一些數(shù)學(xué)家開始利用神經(jīng)網(wǎng)絡(luò)來增強(qiáng)他們的探索能力。
例如，澳大利亞悉尼大學(xué)的喬治·威廉姆森（Geordie Williamson）與DeepMind的研究人員合作，他們在表示論領(lǐng)域研究了特定類型的圖與單變量多項(xiàng)式（Kazhdan-Lusztig多項(xiàng)式）之間的關(guān)系。前者是由節(jié)點(diǎn)和邊組成的復(fù)雜結(jié)構(gòu)，而后者雖然表達(dá)形式簡單，但其中蘊(yùn)含的信息卻難以提取。
DeepMind利用大量數(shù)據(jù)訓(xùn)練神經(jīng)網(wǎng)絡(luò)，使其能夠高精度地預(yù)測這些多項(xiàng)式。分析顯示，某些圖中的邊在預(yù)測中起著關(guān)鍵作用，這一發(fā)現(xiàn)揭示了圖中之前未被注意到的結(jié)構(gòu)。威廉姆森隨后用傳統(tǒng)方法證明了圖與多項(xiàng)式之間的聯(lián)系。這是AI在數(shù)學(xué)領(lǐng)域的一個(gè)創(chuàng)新應(yīng)用，也為后續(xù)研究提供了啟發(fā)。
在2023年6月美國國家科學(xué)院舉辦的AI與數(shù)學(xué)研討會上，威廉姆森提到了這項(xiàng)工作面臨的一些挑戰(zhàn)：比如技術(shù)實(shí)現(xiàn)的細(xì)節(jié)問題可能導(dǎo)致結(jié)果錯(cuò)誤，他懷疑這可能是算法本身的問題還是實(shí)施不當(dāng)所致。他也表示，AI為數(shù)學(xué)研究帶來了新的視角。
符號系統(tǒng)AI帶來的嚴(yán)謹(jǐn)性
在研究的后期階段，數(shù)學(xué)家們更注重清晰性、嚴(yán)謹(jǐn)性和準(zhǔn)確性，這時(shí)符號系統(tǒng)AI發(fā)揮了重要作用。
近年來，一種重要的符號AI應(yīng)用是定理的形式化表達(dá)，即用邏輯系統(tǒng)的形式化語言和語法來表述定理。類似軟件驗(yàn)證工具，證明助手可以驗(yàn)證這些形式化的證明。雖然將自然語言證明轉(zhuǎn)換為機(jī)器可理解的形式化證明是一個(gè)漫長而繁瑣的過程，但隨著新工具的出現(xiàn)，證明助手在數(shù)學(xué)界逐漸得到認(rèn)可。
最常用的證明助手之一是Lean，它由萊昂納多·德·莫拉（Leonardo de Moura）在2010年代初開發(fā)，目前由亞馬遜網(wǎng)絡(luò)服務(wù)公司維護(hù)。Mathlib是一個(gè)基于Lean的電子知識庫，包含約10萬個(gè)定義和25萬個(gè)定理，涵蓋了標(biāo)準(zhǔn)本科數(shù)學(xué)課程的內(nèi)容以及大量新舊研究成果。
Mathlib未來的應(yīng)用方向尚不明確，但正如英國帝國理工學(xué)院的凱文·巴扎德（Kevin Buzzard）所言：“Mathlib正在‘?dāng)?shù)字化’數(shù)學(xué)——就像Spotify數(shù)字化音樂一樣。雖然還不確定具體會帶來什么變化，但我相信這肯定會改變數(shù)學(xué)領(lǐng)域。”
加州大學(xué)洛杉磯分校的菲爾茲獎(jiǎng)得主陶哲軒（Terence Tao）領(lǐng)導(dǎo)的Equational Theories Project（ETP）項(xiàng)目則嘗試通過大規(guī)模計(jì)算生成新的數(shù)學(xué)知識。該項(xiàng)目專注于代數(shù)結(jié)構(gòu)方程之間的邏輯關(guān)系。對于最多包含四個(gè)變量的方程，存在大約4700種這樣的關(guān)系。50名團(tuán)隊(duì)成員在不到六個(gè)月內(nèi)利用強(qiáng)大計(jì)算資源找到了所有這些關(guān)系。
陶哲軒指出，傳統(tǒng)上數(shù)學(xué)家通常是逐一解決問題，而ETP則通過團(tuán)隊(duì)協(xié)作快速生成了大量新知識。他稱：“僅靠人類是無法完成這項(xiàng)工作的。”
安德烈·鮑爾（Andrej Bauer）開玩笑說，未來ChatGPT可能會生成大量虛假的數(shù)學(xué)論文，干擾真正的數(shù)學(xué)研究。不過他相信，機(jī)械化的驗(yàn)證機(jī)制（如Lean）有助于確保結(jié)果的準(zhǔn)確性。
LLMs的進(jìn)步
未來大型語言模型（LLMs）能否將神經(jīng)網(wǎng)絡(luò)AI和符號系統(tǒng)AI結(jié)合起來，服務(wù)于數(shù)學(xué)研究？雖然有可能，但那還需要很長時(shí)間。在2025年的國際數(shù)學(xué)奧林匹克競賽中，LLMs取得了優(yōu)異成績，但比賽題目仍局限于高中數(shù)學(xué)水平。
隨著LLMs在這些任務(wù)上的不斷進(jìn)步，現(xiàn)在需要更具有挑戰(zhàn)性的測試標(biāo)準(zhǔn)。2025年，一個(gè)由40位數(shù)學(xué)家組成的團(tuán)隊(duì)在FrontierMath非營利組織的支持下制定了新的測試標(biāo)準(zhǔn)。
這些測試題難度較高，需要數(shù)學(xué)家掌握相關(guān)文獻(xiàn)并運(yùn)用多種非傳統(tǒng)方法。它們并非陷阱題，而是為了檢驗(yàn)AI的能力和局限性。例如，測試結(jié)果需要是一個(gè)難以猜測的數(shù)字。
每個(gè)測試題的制定都是一項(xiàng)平衡工作。參與開發(fā)的肯·奧諾（Ken Ono）表示：“找到讓模型真正動腦筋的問題非常困難。”2025年12月，奧諾離開了學(xué)術(shù)界，加入了一家AI初創(chuàng)公司Axiom Math。
在2025年5月于伯克利舉行的FrontierMath會議上，奧諾看到自己設(shè)計(jì)的測試題被ChatGPT的升級版本o4-mini成功解決。他說：“AI能在短短10分鐘內(nèi)獨(dú)立完成這個(gè)問題，確實(shí)令人印象深刻。”
新工具帶來的新挑戰(zhàn)
奧諾還提到，與o4-mini的互動讓他感到既興奮又擔(dān)憂：他可以讓AI總結(jié)已知的研究方法，并將其應(yīng)用于完全陌生的數(shù)學(xué)領(lǐng)域。雖然AI在某些方面很有幫助，但真正的創(chuàng)新仍依賴于數(shù)學(xué)家自身的創(chuàng)造力。
盡管這些工具非常實(shí)用，奧諾指出：“目前還沒有AI生成的完全原創(chuàng)的數(shù)學(xué)成果。”他認(rèn)為，真正的數(shù)學(xué)創(chuàng)新來自于數(shù)學(xué)家自己提出的新概念和聯(lián)系。
阿林·杰克遜（Allyn Jackson）是一位專注于科學(xué)和數(shù)學(xué)領(lǐng)域的德國記者。
