? ??導(dǎo)讀

幾個(gè)世紀(jì)以來，計(jì)算機(jī)（機(jī)器）一直是數(shù)學(xué)家的好朋友，他們利用它計(jì)算、提出猜想以及進(jìn)行數(shù)學(xué)證明。隨著交互式定理證明器、機(jī)器學(xué)習(xí)算法和生成式AI等更為先進(jìn)的工具的出現(xiàn)，機(jī)器被更具創(chuàng)新性和深度的方式得到運(yùn)用。近日，在MSRI（美國數(shù)學(xué)科學(xué)研究所，現(xiàn)改名SLMath）四十周年慶典上，陶哲軒（Terence Tao）對(duì)機(jī)器輔助數(shù)學(xué)證明的歷史和最新發(fā)展進(jìn)行概述，并對(duì)數(shù)學(xué)中的機(jī)器輔助將扮演的未來角色進(jìn)行預(yù)測。他表示：早期的計(jì)算機(jī)輔助的數(shù)學(xué)研究以女性為主，并衍生出了一個(gè)計(jì)算能力單位：“千女時(shí)”，一千個(gè)使用加法器的女性能完成多少計(jì)算?！扒畷r(shí)”的出現(xiàn)也標(biāo)志著大規(guī)模計(jì)算的起源。而現(xiàn)在的計(jì)算機(jī)已經(jīng)超越了“暴力窮舉”，它逐漸能夠提供創(chuàng)造性的建議，幫助人們在數(shù)學(xué)研究中找到新的方向和靈感。尤其是GPT-4：“與這些先進(jìn)的語言模型進(jìn)行對(duì)話，能以間接的方式激發(fā)其數(shù)學(xué)思維，它就像一個(gè)非常耐心的同事，善于傾聽而不評(píng)判?！?/span>對(duì)于未來計(jì)算機(jī)在數(shù)學(xué)中作用，陶哲軒說道：“人類與計(jì)算機(jī)在數(shù)學(xué)創(chuàng)造領(lǐng)域的貢獻(xiàn)比是95%和5%，那么在過十年或者二十年，這個(gè)比例就會(huì)變成五五開”。推薦理由：希望以此為契機(jī)，呼吁研究者關(guān)注AI在輔助數(shù)學(xué)證明方面發(fā)揮的驚人作用，機(jī)器學(xué)習(xí)提供了強(qiáng)大的框架，為數(shù)學(xué)家開辟了新思路。未來，AI有巨大的潛能幫助解決那些對(duì)人類來說極具挑戰(zhàn)性的數(shù)學(xué)難題，模擬和執(zhí)行高級(jí)數(shù)學(xué)運(yùn)算，乃至提出新的數(shù)學(xué)猜想和理論。以下為演講全文，編輯做了不改變原意的編譯，請(qǐng)欣賞：

視頻地址：https://vimeo.com/817520060曾有人詢問我美國數(shù)學(xué)科學(xué)研究所（MSRI）以及數(shù)學(xué)的發(fā)展方向時(shí)，我認(rèn)為計(jì)算機(jī)在數(shù)學(xué)領(lǐng)域的應(yīng)用和作用將會(huì)變得越來越重要。計(jì)算機(jī)已經(jīng)在數(shù)學(xué)交流中發(fā)揮出重要的作用，例如用LaTeX進(jìn)行寫作，用電子郵件、視頻會(huì)議與合作者進(jìn)行溝通。在純數(shù)學(xué)方面，計(jì)算機(jī)的作用還沒受到重視，但情況正在改變。

過去，人類與計(jì)算機(jī)在數(shù)學(xué)創(chuàng)造領(lǐng)域的貢獻(xiàn)比是95%和5%，那么在過十年或者二十年，這個(gè)比例就會(huì)變成五五開。要達(dá)到5（人）:95（計(jì)算機(jī)），可能還需要花費(fèi)很長的時(shí)間。

早期的機(jī)器與數(shù)學(xué)：人工的、機(jī)械的，女性主導(dǎo)的

早期計(jì)算機(jī)的關(guān)鍵詞是人工、機(jī)械，在18和19世紀(jì)，計(jì)算機(jī)的主要作用是進(jìn)行數(shù)字計(jì)算、建立對(duì)數(shù)表和三角函數(shù)表。

在20世紀(jì)20年代，物理學(xué)家亨德里克·洛倫茲利用人工計(jì)算機(jī)團(tuán)隊(duì)來模擬大壩（阿夫斯呂伊特戴克）周圍的水流。這是一個(gè)重要的工程項(xiàng)目，需要進(jìn)行大量復(fù)雜的計(jì)算，洛倫茲和他的團(tuán)隊(duì)采用了浮點(diǎn)運(yùn)算，這是一種在當(dāng)時(shí)并不常見的計(jì)算方法。

在戰(zhàn)爭前計(jì)算機(jī)已經(jīng)可以部分求解偏微分方程了。在第一次世界大戰(zhàn)和第二次世界大戰(zhàn)中，計(jì)算機(jī)幫助人類在彈道學(xué)、導(dǎo)航、曼哈頓計(jì)劃等方面進(jìn)行了大量的數(shù)學(xué)計(jì)算。實(shí)際上，大部分工作是由人工計(jì)算機(jī)完成的，這些人工計(jì)算機(jī)主要由女性操作。因?yàn)楫?dāng)時(shí)的男性正在參戰(zhàn)。這也衍生出了一個(gè)計(jì)算能力單位：“千女時(shí)”，一千個(gè)使用加法器的女性能完成多少計(jì)算?！扒畷r(shí)”的出現(xiàn)也標(biāo)志著大規(guī)模計(jì)算的起源。

圖注：高斯和勒讓德利用了素?cái)?shù)表（達(dá)到大約10^6）來研究一個(gè)基本問題：在給定閾值x之前有多少個(gè)素?cái)?shù)（記作π(x)）

研究型數(shù)學(xué)家是如何使用計(jì)算機(jī)的呢？除了建立表格等之外，最早的用途之一就是做出猜想。18世紀(jì)高斯和勒讓德（Gauss and Legendre）在研究素?cái)?shù)時(shí)利用大規(guī)模人工計(jì)算機(jī)構(gòu)建了大量素?cái)?shù)的表格，用于“猜想”素?cái)?shù)分布的規(guī)律。

圖注：勒讓德的素?cái)?shù)分布猜想公式盡管勒讓德的素?cái)?shù)分布猜想在精確性上存在一些問題，但它的影響力仍然非常大。后來，這個(gè)猜想被狄利克雷修正為一個(gè)更準(zhǔn)確的形式，這個(gè)形式現(xiàn)在已經(jīng)被廣泛接受并被納入教科書。

圖注：狄利克雷修正后的公式計(jì)算機(jī)加持下的數(shù)值計(jì)算現(xiàn)在已經(jīng)成為解析數(shù)論中的常規(guī)工具，被用來幫助形成和驗(yàn)證猜想。伯奇和斯溫內(nèi)頓-戴爾猜想就是一個(gè)很好的例子，這個(gè)未解的數(shù)學(xué)問題是通過大量的數(shù)值計(jì)算和數(shù)據(jù)分析來提出的。

圖注：能量均分定理表達(dá)式

電子計(jì)算機(jī)時(shí)代：點(diǎn)開多項(xiàng)數(shù)學(xué)輔助技能樹

在二戰(zhàn)后，物理學(xué)家恩里科·費(fèi)米（Enrico Fermi）、約翰·帕斯塔（John Pasta）、斯坦尼斯洛·烏拉姆（Stanislaw Ulam）和程序員瑪麗·青果（Mary?Tsingou）為了給電子計(jì)算機(jī)“MANIAC”找到新的應(yīng)用，決定模擬晶體的演變。他們將晶體視為一串一維粒子，這些粒子通過哈密頓方程進(jìn)行演變。按照能量均分定理，所有的能量應(yīng)該勻地分散在所有模式（即晶體中的各個(gè)粒子）中。

圖注：實(shí)驗(yàn)結(jié)果表示能量并不均分，找到的是穩(wěn)定局部解（孤波）但實(shí)際運(yùn)行數(shù)值模擬時(shí)，結(jié)果并未符合他們預(yù)期的能量均分定理。起初，他們設(shè)定了一個(gè)初始狀態(tài)，其中只有一個(gè)粒子的能量被激發(fā)。然而，隨著時(shí)間的推移，能量并沒有均勻分布，而是出現(xiàn)了在某一兩個(gè)粒子之間的長期穩(wěn)定。也就是就是出現(xiàn)了孤波（或叫孤子）的現(xiàn)象。

然而，用計(jì)算機(jī)進(jìn)行長時(shí)間運(yùn)行實(shí)驗(yàn)，現(xiàn)象會(huì)消失，能量最終會(huì)均勻分布。

這種現(xiàn)象的出現(xiàn)是因?yàn)樗麄冄芯康南到y(tǒng)其實(shí)是一個(gè)完全可積系統(tǒng)——投達(dá)晶格方程（Toda lattice equations）亦稱投達(dá)鏈——的近似。在這個(gè)完全可積系統(tǒng)中，孤子是會(huì)永久存在的。而他們實(shí)際的系統(tǒng)并不是完全可積的，但卻足夠接近，以至于他們能在模擬實(shí)驗(yàn)中看到孤子現(xiàn)象。

這個(gè)具有巨大影響力的數(shù)值實(shí)驗(yàn)開啟了可積系統(tǒng)的研究，也開啟了孤波的穩(wěn)定性研究，這個(gè)研究領(lǐng)域至今仍然活躍。

圖注：阿佩爾和沃夫?qū)す显?976年用計(jì)算機(jī)輔助證明了四色定理。

在現(xiàn)代電子計(jì)算機(jī)的初期，計(jì)算機(jī)的威力在于它們能夠揭示出一些“意料”之外的現(xiàn)象。四色定理可能是大家最熟知的一個(gè)通過計(jì)算機(jī)得證的定理。在其證明中，凱尼斯·阿佩爾（Kenneth Appel）和沃夫?qū)す?/span>（Wolfgang Haken）編寫了一些特定的程序，這些程序可以處理特定的圖，并通過計(jì)算機(jī)檢查這些圖的某些性質(zhì)。如果某一特定的圖能夠滿足這些性質(zhì)，那么就能用四種顏色來對(duì)其進(jìn)行著色。這就是通過計(jì)算機(jī)得以證明的四色定理。四色定理的證明分為兩個(gè)主要部分：可歸化和不可避免性。可歸化部分表明，任何包含1834種配置中的任何一種的圖都可以轉(zhuǎn)換為更小的圖，且如果更小的圖可以四色著色，那么原圖也可以。這部分證明是通過將這些配置逐個(gè)輸入計(jì)算機(jī)完成的。不可避免性部分表明，如果存在一個(gè)不能四色著色的圖，那么它必須包含1834種配置中的至少一種，這部分通過手動(dòng)檢查超過400頁的微縮膠片來驗(yàn)證。

從現(xiàn)在的標(biāo)準(zhǔn)來看，Appel-Haken的原始證明含有一些可修復(fù)的錯(cuò)誤，并不符合現(xiàn)代的計(jì)算機(jī)可驗(yàn)證證明的標(biāo)準(zhǔn)。1996年，羅伯遜（Robertson）、桑德斯（Sanders）、西蒙（Seymour）和托馬斯（Thomas）首次提出了一個(gè)真正的計(jì)算機(jī)可驗(yàn)證的證明，他們使用633種配置，這些配置的可歸化和不可避免性都可由計(jì)算機(jī)檢查。然后在2005年，維爾納（Werner）和貢蒂埃（Gonthier）使用輔助工具Coq完全形式化了這個(gè)證明，使其成為一個(gè)真正的計(jì)算機(jī)可驗(yàn)證的證明。

開普勒猜想是另一個(gè)計(jì)算機(jī)輔助數(shù)學(xué)證明的例子。在17世紀(jì)，開普勒研究了三維空間中單位球體的最密集堆積方式，發(fā)現(xiàn)兩種堆積方式，即六方緊密堆積和立方緊密堆積，它們的密度都約為74%。開普勒猜測這是堆積密度的最大可能值，沒有其他堆積方式可以超過這個(gè)密度。這個(gè)猜想至今仍是一個(gè)重要的數(shù)學(xué)問題。
開普勒猜想本質(zhì)上是一個(gè)涉及無窮多變量的優(yōu)化問題，這使得它并不容易通過計(jì)算機(jī)驗(yàn)證。盡管在1951年，Toth提出了一種可能的解決方法，即通過有限多個(gè)沃羅諾伊單元的體積上的某些加權(quán)不等式來尋找球體堆積密度的上界，但是，盡管經(jīng)過多次嘗試，但并沒有找到能得出精確結(jié)果的有說服力的證明。托馬斯·海爾斯（Thomas Hales）和塞繆爾·弗格森（Samuel Ferguson）采取了一種靈活求解最小化問題的策略：調(diào)整評(píng)分函數(shù)，但這反過來又會(huì)產(chǎn)生更多的問題。然而，盡管評(píng)分函數(shù)變得越來越復(fù)雜，但他們的任務(wù)在某種程度上卻變簡單了。數(shù)篇論文發(fā)表后，兩位學(xué)者終在1998年成功證明了開普勒猜想，證明方式是用線性規(guī)劃設(shè)計(jì)出了一個(gè)復(fù)雜的評(píng)分函數(shù)。

據(jù)說，海爾斯最初并不打算使用計(jì)算機(jī)來幫助他證明這個(gè)猜想，但隨著項(xiàng)目變得越來越復(fù)雜，他發(fā)現(xiàn)他必須要依賴計(jì)算機(jī)。最后他們的證明包含了250頁的數(shù)學(xué)筆記，以及3GB的計(jì)算機(jī)代碼、數(shù)據(jù)和結(jié)果。

為“打消”對(duì)開普勒猜想證明的疑慮，托馬斯·海爾斯在2003年啟動(dòng)“Flyspeck”項(xiàng)目。他們使用證明助手的語言（the language of a proof assistant）來形式化證明過程，使得計(jì)算機(jī)能夠自動(dòng)進(jìn)行驗(yàn)證。雖然最初估計(jì)項(xiàng)目需要二十年，但通過海爾斯和他的21位合作者的共同努力，項(xiàng)目在2014年完成。

近年來，彼得·舒爾茨（Peter Scholze）的液態(tài)張量實(shí)驗(yàn)無疑是最為人所知的形式化證明實(shí)驗(yàn)項(xiàng)目，涉及舒爾茨的"凝聚態(tài)數(shù)學(xué)"理論（condensed mathematics），目標(biāo)是修復(fù)拓?fù)淇臻g類別的一些問題，如拓?fù)浒⒇悹柸?，方式是使用“凝聚”的新的?shù)學(xué)對(duì)象來替代傳統(tǒng)的拓?fù)淇臻g類別。

“凝聚數(shù)學(xué)”理論中的一個(gè)關(guān)鍵結(jié)果是“消失定理”，?研究發(fā)現(xiàn)，在特定的數(shù)學(xué)結(jié)構(gòu)中，某些元素或?qū)傩栽谝欢l件下會(huì)“消失”。消失定理是凝聚數(shù)學(xué)中的核心，它是使用凝聚數(shù)學(xué)進(jìn)行泛函分析研究的基礎(chǔ)。證明這個(gè)定理非常困難，舒爾茨花了一年研究，但進(jìn)展緩慢。

于是，舒爾茨發(fā)起“液態(tài)張量實(shí)驗(yàn)”，希望用數(shù)學(xué)軟件Lean對(duì)結(jié)果進(jìn)行形式化，實(shí)現(xiàn)過程中，他們將幾個(gè)基礎(chǔ)的數(shù)學(xué)理論添加到了Lean的mathlib庫中。最后，在舒爾茨和其團(tuán)隊(duì)的努力下，2021年5月，形式化了一個(gè)關(guān)鍵的子定理，2022年7月得到了完整定理的形式化。該項(xiàng)目的主要成就在于大幅擴(kuò)充了Lean的數(shù)學(xué)庫。事實(shí)上，由于該項(xiàng)目構(gòu)建的豐富庫例程，其他的Lean形式化項(xiàng)目變得更加便捷和高效。

圖注：液態(tài)張量實(shí)驗(yàn)藍(lán)圖

形式化的過程同時(shí)伴隨著一個(gè)人類可讀的證明“藍(lán)圖”創(chuàng)建。這個(gè)"藍(lán)圖"以一種交互式的方式合成了正式和非正式的證明，這讓舒爾茨和其他人能夠更深入地理解這個(gè)證明。

圖注：利用Lean證明拓?fù)涠ɡ?。陶哲軒設(shè)想，未來的拓?fù)鋵W(xué)教科書可能會(huì)使用這種交互式的步驟來解釋證明，使學(xué)習(xí)過程更為清晰和簡單。

受到這項(xiàng)工作的啟發(fā)，越來越多的研究者正在開發(fā)軟件工具，希望能夠自動(dòng)將形式化的證明轉(zhuǎn)化為人類可讀的交互式證明。

計(jì)算機(jī)作為輔助工具，通常發(fā)揮的作用方式有兩種：1.逐漸增加形式化證明的使用；2.使用計(jì)算機(jī)進(jìn)行暴力計(jì)算。例如2013年Helfgott解決奇數(shù)哥德巴赫猜想所使用的方案就是暴力計(jì)算+巧妙的優(yōu)化。

人工智能時(shí)代：神經(jīng)網(wǎng)絡(luò)與大模型走進(jìn)數(shù)學(xué)

我特別喜歡的例子是2016年的拉姆齊定理。先來看“布爾型畢達(dá)哥拉斯三元組問題”，它的內(nèi)容大致是這樣的：如果你把1到7825這些數(shù)字分成兩組（也就是用兩種顏色進(jìn)行標(biāo)記），那么無論如何分組，你都能在其中一組找到至少一組畢達(dá)哥拉斯三元組（滿足a2 + b2 = c2的三個(gè)數(shù)），并且這三個(gè)數(shù)是同一顏色（在同一組里）。這實(shí)際上是一個(gè)計(jì)算量非常大的3-SAT問題（3-可滿足性問題，NP完全問題的一個(gè)例子），解決他并不能應(yīng)用標(biāo)準(zhǔn)的3-SAT求解器，需要對(duì)3-SAT求解器進(jìn)行特殊的定制或修改。最后，胡埃萊（Huele），庫爾曼（Kullman）和馬雷克（Marek）利用計(jì)算機(jī)解決了這個(gè)問題。他們使用了一種叫做"布爾滿足性求解器"的工具，在Stampede超級(jí)計(jì)算機(jī)上運(yùn)行了四年，最終找到了所有可能的分組方式，并證明了無論如何分組，總能在其中一組找到至少一個(gè)同色的畢達(dá)哥拉斯三元組。這個(gè)證明的數(shù)據(jù)量非常大，原始數(shù)據(jù)大小達(dá)到了200TB，但是可以通過壓縮降低到68GB。在流體方程中，有兩個(gè)著名的未解問題：納維-斯托克斯方程（Navier-Stokes equations）和歐拉方程（Euler equations）的有限時(shí)間爆炸。十年前，數(shù)值模擬給出了一些看似發(fā)展出奇異性的解：它們開始時(shí)是平滑的，但隨著時(shí)間推移變得越來越湍流，能量開始集中在某些特定的點(diǎn)。但是，由于計(jì)算精度的限制，當(dāng)模擬接近奇異性發(fā)生時(shí)，這些數(shù)值結(jié)果就變得不可靠。學(xué)界認(rèn)識(shí)到，如果可以找到一個(gè)特定的類型的解，即自相似解（self-similar solutions），那么就可能證明流體方程在有限時(shí)間內(nèi)發(fā)展出奇異性。這類似于在廣義相對(duì)論中尋找閉合的測地線（geodesic）或軌道。使用計(jì)算機(jī)能找到一個(gè)“近似”的自相似解。這個(gè)解并不完美，但接近完美的自相似解，只有微小的誤差。但如果能結(jié)合嚴(yán)格的穩(wěn)定性分析，就可以證明實(shí)際自相似解的存在。這是理想化的方法，可視為“夢想”，在實(shí)際操作中可能很難實(shí)現(xiàn)。在2022年，發(fā)展出了兩種求自相似解的方法：1. 陳-侯方法，采用傳統(tǒng)的數(shù)值偏微分方程，通過計(jì)算機(jī)輔助進(jìn)行嚴(yán)格的穩(wěn)定性分析，這是首次為不可壓縮歐拉方程的光滑解在圓柱邊界之外建立有限時(shí)間爆破結(jié)果的嚴(yán)格證明；2. 王-賴-戈麥斯-塞拉諾-巴克馬斯特方法：使用了物理信息神經(jīng)網(wǎng)絡(luò)（PINN，Physics Informed Neural Network），這是一種結(jié)合物理學(xué)知識(shí)與神經(jīng)網(wǎng)絡(luò)的技術(shù)。

也有許多研究人員正在積極運(yùn)用機(jī)器輔助技術(shù)來探尋流體方程的“爆破解”。但是，流體動(dòng)力學(xué)中的一個(gè)非常復(fù)雜問題：納維-斯托克斯方程的全局規(guī)律性，目前似乎仍然難以解決。

在結(jié)論理論（knot theory）領(lǐng)域中，計(jì)算機(jī)和人類數(shù)學(xué)方法發(fā)生了有趣結(jié)合。結(jié)論理論研究的是，將線纏繞在空間中形成的結(jié)的性質(zhì)。學(xué)界目前努力在將結(jié)論的雙曲不變量（由實(shí)數(shù)和復(fù)數(shù)組成的集合）與結(jié)論的簽名（一個(gè)整數(shù)）聯(lián)系起來，以更好地理解結(jié)的性質(zhì)和結(jié)構(gòu)。代表工作由亞歷克斯·戴維斯（Alex Davies）等人的團(tuán)隊(duì)作出。他們最近的進(jìn)展是人工神經(jīng)網(wǎng)絡(luò)所帶來的。他們使用神經(jīng)網(wǎng)絡(luò)，在包含超過兩百萬個(gè)“結(jié)”的數(shù)據(jù)庫上訓(xùn)練。訓(xùn)練后的神經(jīng)網(wǎng)絡(luò)非常成功，能夠準(zhǔn)確預(yù)測從雙曲不變量到簽名的轉(zhuǎn)換。這也表明雙曲不變量和簽名之間確實(shí)有聯(lián)系。

然而，神經(jīng)網(wǎng)絡(luò)的工作方式就像一個(gè)“黑盒子”，可以看到它的輸入和輸出，但是里面究竟發(fā)生了什么，人們并不知道。因此，雙曲不變量和簽名之間的具體關(guān)系，目前也無法通過人工神經(jīng)網(wǎng)絡(luò)得知。

圖注：用于預(yù)測簽名的主要雙曲不變量于是，他們進(jìn)行顯著性性分析，來確定哪些雙曲不變量對(duì)預(yù)測簽名的關(guān)系最重要。換句話說，他們想知道改變哪些輸入?yún)?shù)會(huì)對(duì)輸出結(jié)果產(chǎn)生最大的影響。最終，他們發(fā)現(xiàn)24個(gè)雙曲不變量中只有3個(gè)對(duì)預(yù)測簽名的關(guān)系有顯著影響。這意味著，盡管他們一開始可能以為所有的不變量都很重要，但實(shí)際上只有其中的一小部分真正關(guān)鍵。因此，神經(jīng)網(wǎng)絡(luò)+顯著性分析有助于更深入地了解這雙曲不變量和簽名之間的關(guān)系。使用類似于“整數(shù)序列在線百科全書（Online Encyclopedia of Integer Sequences）”的特殊數(shù)據(jù)庫可以挖掘數(shù)學(xué)中不同領(lǐng)域間的隱秘聯(lián)系。這樣的聯(lián)系可能表現(xiàn)為兩個(gè)完全不同的領(lǐng)域產(chǎn)生相同的數(shù)字序列，就像數(shù)學(xué)中著名的“怪獸月光理論（Monstrous moonshine）”現(xiàn)象那樣。

未來，希望有更多自動(dòng)化工具能夠在更深的層面上發(fā)現(xiàn)不同領(lǐng)域之間的聯(lián)系，例如兩篇來自不同領(lǐng)域的論文可能證明了相似的定理，那么這些工具能夠清晰“識(shí)別”。盡管這樣的“語義搜索”技術(shù)可能還需要至少一年的時(shí)間才能實(shí)現(xiàn)，但它展示了一種令人充滿期待的未來趨勢。

圖注：GPT-4解決數(shù)學(xué)問題大模型在數(shù)學(xué)研究過程中也表現(xiàn)出了一些潛力，例如GPT-4甚至可以解決2022年國際數(shù)學(xué)奧林匹克競賽中的問題，展現(xiàn)了其在數(shù)學(xué)領(lǐng)域的應(yīng)用能力。

圖注：大模型最初給出的答案是120但這個(gè)系統(tǒng)在處理數(shù)學(xué)問題時(shí)并不穩(wěn)定。雖然它有時(shí)候出人意料，但同時(shí)也可能在解釋或計(jì)算數(shù)學(xué)概念方面產(chǎn)生錯(cuò)誤，甚至在處理基本算術(shù)問題時(shí)也會(huì)出錯(cuò)（如7*4+8*8=120的錯(cuò)誤）。因此，當(dāng)前的技術(shù)水平可以看做“困惑的本科生”，雖然已經(jīng)記憶了所有內(nèi)容卻不真正理解。

有學(xué)者嘗試通過一些新的方法來讓那些大語言模型變得更懂?dāng)?shù)學(xué)，包括與Wolfram Alpha等傳統(tǒng)計(jì)算工具結(jié)合以及融合傳統(tǒng)數(shù)學(xué)解題策略。除此之外，與這些先進(jìn)的語言模型進(jìn)行對(duì)話也能以間接的方式激發(fā)其數(shù)學(xué)思維，它就像一個(gè)非常耐心的同事，善于傾聽而不評(píng)判。大模型表現(xiàn)出的這一特點(diǎn)，也能促進(jìn)人類探索新想法和創(chuàng)造性思考。

總結(jié)：鼓勵(lì)嘗試人工智能工具

那么，計(jì)算機(jī)輔助證明現(xiàn)在進(jìn)展到什么地步了？首先明確它還似乎不太可能獨(dú)立解決主要的數(shù)學(xué)問題；拋開前面那個(gè)奧林匹克問題不談，如果你向ChatGPT簡單輸入“請(qǐng)為我解決黎曼猜想”，可能得到似是而非的胡言亂語。其次它越來越多地被用于支持人類數(shù)學(xué)家的工作，與暴力窮舉或計(jì)算不同，現(xiàn)在的計(jì)算機(jī)逐漸能夠提供創(chuàng)造性的建議，幫助人們在數(shù)學(xué)研究中找到新的方向和靈感。總結(jié)一下，人工智能技術(shù)，在短期內(nèi)，可能在數(shù)學(xué)研究的輔助方面產(chǎn)生更多影響，例如自動(dòng)總結(jié)大量文獻(xiàn)或建議相關(guān)工作，但它還無法觸及核心方面。我鼓勵(lì)大家嘗試人工智能工具，它與我們通常使用的挑剔工具（如LaTeX，一個(gè)括號(hào)可能導(dǎo)致全盤錯(cuò)誤）不同，能夠容忍非常模糊的輸入，并從中得到結(jié)構(gòu)化和有趣的答案。

本文經(jīng)授權(quán)轉(zhuǎn)載自微信公眾號(hào)“智源社區(qū)”。