新智元報(bào)道
編輯：Aeneas 好困
【新智元導(dǎo)讀】毫無(wú)疑問(wèn)，數(shù)學(xué)家的工作方式，正在被AI顛覆！陶哲軒轉(zhuǎn)發(fā)的這期美國(guó)數(shù)學(xué)學(xué)會(huì)通報(bào)，大咖云集，星光璀璨。針對(duì)AI改變數(shù)學(xué)的議題，他們中有降臨派，也有懷疑論者。而陶哲軒也直接高呼：這個(gè)領(lǐng)域太快了，現(xiàn)在我沒(méi)發(fā)表的論文已經(jīng)不夠看了！
AI，的確正在改變數(shù)學(xué)。
最近，一直十分關(guān)注這個(gè)議題的陶哲軒，轉(zhuǎn)發(fā)了最近一期的《美國(guó)數(shù)學(xué)學(xué)會(huì)通報(bào)》（Bulletin of the American Mathematical Society）。
圍繞「機(jī)器會(huì)改變數(shù)學(xué)嗎？」這個(gè)話(huà)題，眾多數(shù)學(xué)家發(fā)表了自己的觀點(diǎn)，全程火花四射，內(nèi)容硬核，精彩紛呈。
作者陣容大咖云集，包括菲爾茲獎(jiǎng)得主Akshay Venkatesh、華裔數(shù)學(xué)家鄭樂(lè)雋、紐大計(jì)算機(jī)科學(xué)家Ernest Davis等多位業(yè)界知名學(xué)者。
要知道，其中很多文章是在一年前提交的，而一年之內(nèi)，AI的世界已經(jīng)發(fā)生了天翻地覆的變化，其中某些內(nèi)容可能已經(jīng)略顯過(guò)時(shí)了。
然而，盡管如此，這些文章依舊含金量滿(mǎn)滿(mǎn)，甚至讓陶哲軒高呼：這個(gè)領(lǐng)域太快了！讓我還沒(méi)發(fā)表的文章顯得有些多余。
無(wú)人可以否認(rèn)，如今AI工具正在讓數(shù)學(xué)領(lǐng)域以驚人的速度向前邁進(jìn)。
人工智能是否將引領(lǐng)包括純數(shù)學(xué)在內(nèi)的科學(xué)領(lǐng)域，在信息收集和處理方式上的一場(chǎng)革命？它會(huì)改變數(shù)學(xué)研究方法嗎？
對(duì)此，數(shù)學(xué)家們的意見(jiàn)產(chǎn)生了分歧：某些人認(rèn)為，機(jī)器學(xué)習(xí)在研究中的廣泛應(yīng)用即將到來(lái)，而另一些人則持懷疑態(tài)度，他們回顧了1960年代的過(guò)度樂(lè)觀和隨后的「AI寒冬」。
然而，數(shù)學(xué)研究實(shí)踐中，已經(jīng)極有可能發(fā)生劇變。現(xiàn)在，數(shù)學(xué)家們是時(shí)候考慮這些變化所帶來(lái)的問(wèn)題了。
不用懷疑，風(fēng)暴就在前方。
那么，機(jī)器會(huì)改變數(shù)學(xué)嗎？
數(shù)學(xué)自動(dòng)化對(duì)數(shù)學(xué)研究的影響
在這篇論文中，菲爾茲獎(jiǎng)得主Akshay Venkatesh探討了自動(dòng)化對(duì)數(shù)學(xué)研究的影響。
在這篇論文中，Akshay Venkatesh提出了一個(gè)有趣的思想實(shí)驗(yàn)
2017年，DeepMind的Alphazero一夜之間自學(xué)了國(guó)際象棋和圍棋，超越了人類(lèi)。
如果十年后，「Alephzero」（寫(xiě)作
），也做了同樣的格式化數(shù)學(xué)呢？
本文中的「數(shù)學(xué)」指的是「純數(shù)學(xué)研究」。
我們的出發(fā)點(diǎn)是假設(shè)「Alephzero」自學(xué)了高中和大學(xué)數(shù)學(xué)，并做完了SpringerVerlag Graduate Terts in Mathematics 系列的所有習(xí)題。第二天早上，數(shù)學(xué)家們將它放出，下載它的孩子們，用我們的計(jì)算資源運(yùn)行它們。
這的確是一個(gè)思想實(shí)驗(yàn)，因?yàn)樗@然是不現(xiàn)實(shí)的：通過(guò)把我們的視野限制在未來(lái)的十年或二十年，我們?cè)试S自己脫離可能伴隨這種技術(shù)進(jìn)步而發(fā)生的社會(huì)變革來(lái)考慮這個(gè)問(wèn)題，也允許我們避免思考更極端的機(jī)器智能類(lèi)型，我們把「Alephzero」當(dāng)作一個(gè)電動(dòng)工具而不是一個(gè)有生命的合作者來(lái)建模。
我們可以這樣安慰自己：實(shí)際上，這個(gè)前提離我們太遙遠(yuǎn)了，我們不需要考慮它。但是，如果我們?cè)试S哪怕是微乎其微的可能性，這種情況可能會(huì)在二十年后發(fā)生。
通過(guò)數(shù)學(xué)家和問(wèn)題網(wǎng)絡(luò)中的貝葉斯相互作用，提供了一個(gè)非常粗略的模型，展示了我們的部分價(jià)值機(jī)制。我們現(xiàn)在考慮「Alephzero」將如何影響這個(gè)網(wǎng)絡(luò)并改變結(jié)果。
正如我們所看到的，感知到的困難是我們構(gòu)建價(jià)值的重要組成部分。
無(wú)論具體情況如何，「Alephzero」都會(huì)改變我們解決問(wèn)題的能力，從而改變我們對(duì)問(wèn)題難度的看法。
數(shù)學(xué)過(guò)程中可以加速最快的部分將在其感知難度上降低最大，并且根據(jù)我們上面的模型，狀態(tài)將遭受最大的降低。類(lèi)似的模式發(fā)生在許多自動(dòng)化實(shí)例中。
最后，「Alephzero」將大大擴(kuò)展數(shù)學(xué)上有趣問(wèn)題的整個(gè)范圍。它會(huì)在專(zhuān)業(yè)數(shù)學(xué)家和其他人之間，創(chuàng)造公平的競(jìng)爭(zhēng)環(huán)境。
機(jī)器怎樣讓數(shù)學(xué)更聚合
數(shù)學(xué)家鄭樂(lè)雋認(rèn)為，既然技術(shù)已經(jīng)改變了我們研究數(shù)學(xué)的方式，那就可以利用這項(xiàng)技術(shù)讓數(shù)學(xué)更具「聚合」，而不是讓人類(lèi)數(shù)學(xué)家在面對(duì)技術(shù)進(jìn)步時(shí)變得多余。
在思考「研究數(shù)學(xué)」意味著什么時(shí)，她研究了數(shù)學(xué)技術(shù)的以下幾個(gè)方面：教學(xué)和學(xué)習(xí)、提出問(wèn)題、協(xié)作、傳播和做研究的行為。
這并不是一個(gè)嚴(yán)謹(jǐn)?shù)姆治�，而是基于她作為�?shù)學(xué)家經(jīng)驗(yàn)的明智反思。
鄭樂(lè)雋認(rèn)為，雖然現(xiàn)在有一些計(jì)算機(jī)輔助的校對(duì)檢查器，甚至證明生成器，但技術(shù)還沒(méi)有真正侵占數(shù)學(xué)研究最深刻、最有創(chuàng)意、最人性化的方面。
深層的創(chuàng)造性部分首先涉及提出想法定義的想法、證明的想法、在數(shù)學(xué)的不同部分之間建立聯(lián)系的想法、表達(dá)事物的新方法的想法、符號(hào)和術(shù)語(yǔ)的想法、圖解推理的想法以及視覺(jué)表示的想法。
為了讓機(jī)器做數(shù)學(xué)研究，我們必須想辦法告訴它們?nèi)プ觯?strong>如果我們自己還不知道怎么做，那么我們就很難告訴它們?cè)趺醋觥?/strong>
機(jī)器可以進(jìn)行一定程度的證明檢查，但暗地里，數(shù)學(xué)家們都知道，我們寫(xiě)不出完全嚴(yán)格的證明我們根據(jù)邏輯提出論點(diǎn)，并由我們認(rèn)為同行能夠填寫(xiě)的邏輯步驟來(lái)支持。
我們沒(méi)有定義這些步驟的大小，所以很難告訴機(jī)器去做。
生成證明是一種完全不同的技能，而不僅僅是檢查它們，任何數(shù)學(xué)學(xué)生都知道。能夠遵循別人的證據(jù)，比自己想出一個(gè)新的證據(jù)要容易得多。這并不是說(shuō)計(jì)算機(jī)在數(shù)學(xué)研究能力上永遠(yuǎn)不可能超過(guò)人類(lèi)數(shù)學(xué)家。
在她看來(lái)，計(jì)算機(jī)比人類(lèi)數(shù)學(xué)家更厲害的地方就在于
它們有更大的能力來(lái)搜索所有可能的動(dòng)作，通過(guò)搜索目前已知的所有可能的邏輯結(jié)果，它們就能?chē)L試提出新的數(shù)學(xué)。
這需要想象力、猜測(cè)和直覺(jué)的飛躍，什么足以讓計(jì)算機(jī)做到這一點(diǎn)？這個(gè)想法非常有趣。
計(jì)算機(jī)能幫我們做邏輯推理嗎
計(jì)算機(jī)已經(jīng)徹底變革了我們進(jìn)行數(shù)學(xué)研究的方法，讓復(fù)雜的計(jì)算變得輕而易舉。
但接下來(lái)，它們是否會(huì)成為我們邏輯推理的助手？甚至有朝一日，它們能否獨(dú)立進(jìn)行推理呢？
本文將帶你一覽神經(jīng)網(wǎng)絡(luò)、計(jì)算機(jī)定理證明器以及大語(yǔ)言模型在近期的重要進(jìn)展。
形式化工具如何幫我們更好地做數(shù)學(xué)研究
從20世紀(jì)初開(kāi)始，我們就明白，數(shù)學(xué)定義和證明能夠通過(guò)擁有嚴(yán)格語(yǔ)法和規(guī)則的形式系統(tǒng)得到表示。
在這一基礎(chǔ)上，計(jì)算機(jī)證明助手的發(fā)展讓我們能夠?qū)?shù)學(xué)知識(shí)以數(shù)字化的形式進(jìn)行編碼。
本文將探討這類(lèi)技術(shù)及其相關(guān)工具如何幫助我們更好地進(jìn)行數(shù)學(xué)研究。
用定理證明器，簡(jiǎn)化數(shù)學(xué)研究中的復(fù)雜問(wèn)題
本文探討了如何利用交互式定理證明器通過(guò)設(shè)定抽象邊界來(lái)簡(jiǎn)化數(shù)學(xué)研究中的復(fù)雜問(wèn)題。
奇異的新宇宙：LLM讓數(shù)學(xué)家用更自然的語(yǔ)言和證明助手交流
目前的計(jì)算機(jī)程序，也就是證明助手，能夠校驗(yàn)數(shù)學(xué)證明的正確性，但它們使用的專(zhuān)業(yè)證明語(yǔ)言對(duì)很多數(shù)學(xué)家而言構(gòu)成了一道門(mén)檻。
大語(yǔ)言模型（LLM）具有打破這一障礙的可能性，讓數(shù)學(xué)家們能夠用更自然的語(yǔ)言與證明助手進(jìn)行交流。這樣不僅能夠培養(yǎng)他們的直覺(jué)，還能確保他們的論證過(guò)程正確無(wú)誤。
用深度學(xué)習(xí)工具做純數(shù)學(xué)研究
本文是關(guān)于一位純數(shù)學(xué)家在研究中嘗試使用深度學(xué)習(xí)工具時(shí)，可能會(huì)期待的個(gè)人體驗(yàn)和非正式分享。
AI能做數(shù)學(xué)研究嗎
本文探討了目前AI技術(shù)在解決融合了基礎(chǔ)數(shù)學(xué)和常識(shí)推理的文字題目方面的能力和局限。
作者回顧了三種利用AI自然語(yǔ)言技術(shù)開(kāi)發(fā)的方法：直接給出答案、生成解題的計(jì)算機(jī)程序，以及生成可供自動(dòng)定理驗(yàn)證器使用的形式化表述。
作者認(rèn)為，這些限制在發(fā)展純數(shù)學(xué)研究用的AI技術(shù)中的重要性尚未明確，但它們?cè)跀?shù)學(xué)應(yīng)用中極為關(guān)鍵，并且在開(kāi)發(fā)能夠理解人類(lèi)編寫(xiě)的數(shù)學(xué)內(nèi)容的程序時(shí)也很重要。
機(jī)器時(shí)代下的證明是怎樣的
作者在本文中探討了證明的本質(zhì)及其在機(jī)器時(shí)代的演變，并通過(guò)對(duì)比傳統(tǒng)驗(yàn)證和計(jì)算機(jī)驗(yàn)證中的價(jià)值觀進(jìn)行了分析。
文章最終提出的方法可能使計(jì)算機(jī)證明借鑒人類(lèi)經(jīng)驗(yàn)中的成功策略。
自動(dòng)化，讓數(shù)學(xué)家反思自己的價(jià)值
在這篇論文中，作者嚴(yán)厲地批評(píng)了同行們?nèi)狈λ伎�，尤其是在考慮數(shù)學(xué)的機(jī)械化未來(lái)時(shí)，他們忽視了社會(huì)更廣泛層面上關(guān)于技術(shù)和人工智能的重要辯論。
p-adic數(shù)域中的連分?jǐn)?shù)
連分?jǐn)?shù)在數(shù)論特別是丟番圖逼近這一領(lǐng)域享有悠久的歷史。
本文旨在概述p-adic連分?jǐn)?shù)理論的核心成果，這是一種定義在p-adic數(shù)域Qp上的連分?jǐn)?shù)。
內(nèi)容將從基本概念講起，直至介紹最新進(jìn)展和當(dāng)前面臨的開(kāi)放性問(wèn)題。
陶哲軒發(fā)文：機(jī)器輔助證明
順便，陶哲軒也安利了一下自己之前寫(xiě)的論文「Machine assisted proof」。
論文地址：https://terrytao.files.wordpress.com/2024/03/machine-assisted-proof-notices.pdf
在這篇論文中陶哲軒表示，借助于LLM處理自然語(yǔ)言輸入的能力，它們很可能成為一個(gè)用戶(hù)友好的平臺(tái)，使得那些不具備特定軟件知識(shí)的數(shù)學(xué)家也能夠使用高級(jí)工具。
如今，他和很多科學(xué)家已經(jīng)習(xí)慣使用這些模型來(lái)生成各種語(yǔ)言的簡(jiǎn)單代碼，包括符號(hào)代數(shù)包，或者制作復(fù)雜的圖表和圖像了。
目前，由于形式化證明驗(yàn)證（formal proof verification）工作非常依賴(lài)人力，這使得實(shí)時(shí)將大量當(dāng)前研究論文完全形式化變得不切實(shí)際。
在偏微分方程領(lǐng)域中，常常需要通過(guò)多頁(yè)的計(jì)算來(lái)估計(jì)涉及一個(gè)或多個(gè)未知函數(shù)（比如PDE的解）的積分表達(dá)式。
其中便涉及到使用這些函數(shù)在不同函數(shù)空間范數(shù)（如Sobolev空間范數(shù)）中的界限，結(jié)合標(biāo)準(zhǔn)不等式（例如Hlder不等式和Sobolev不等式），以及諸如分部積分或積分符號(hào)下的微分等恒等式。
這類(lèi)計(jì)算雖然是常規(guī)操作，但可能包含各種程度的錯(cuò)誤（如符號(hào)錯(cuò)誤），對(duì)審稿人來(lái)說(shuō)，細(xì)致地檢查這些計(jì)算既枯燥又費(fèi)時(shí)，而且這些計(jì)算本身除了最終的估計(jì)結(jié)果是正確的之外，很難提供更深入的數(shù)學(xué)理解或見(jiàn)解。
可以設(shè)想，未來(lái)可能開(kāi)發(fā)出工具，以自動(dòng)或半自動(dòng)的方式建立數(shù)學(xué)估計(jì)，并且將目前那些既冗長(zhǎng)又缺乏啟發(fā)性的估計(jì)證明替換為一個(gè)指向形式證明證書(shū)的鏈接。
更進(jìn)一步，我們也許能夠期待，基于一組初始的假設(shè)和方法，未來(lái)的AI工具能夠提出它所能得出的最佳估計(jì)，而無(wú)需先進(jìn)行紙筆計(jì)算來(lái)預(yù)測(cè)這個(gè)估計(jì)可能是什么。
目前來(lái)看，估計(jì)可能的狀態(tài)空間過(guò)于復(fù)雜，難以自動(dòng)化地進(jìn)行探索；但隨著技術(shù)的發(fā)展，實(shí)現(xiàn)這種自動(dòng)化探索的可能性并非遙不可及。
一旦實(shí)現(xiàn)，我們就能在目前看來(lái)不可行的規(guī)模上進(jìn)行數(shù)學(xué)探索。
還是以偏微分方程為例，目前的研究通常一次只研究一到兩個(gè)方程；但在未來(lái)，我們可能能同時(shí)研究數(shù)百個(gè)方程。
例如，先對(duì)一個(gè)方程完整地展開(kāi)論證，然后讓AI工具將這些論證調(diào)整適用于大量相關(guān)的方程族，必要時(shí)，當(dāng)論證的擴(kuò)展出現(xiàn)非常規(guī)情況時(shí)，AI會(huì)向作者提問(wèn)。
如今，在數(shù)學(xué)的其他領(lǐng)域，比如圖論，這種大規(guī)模數(shù)學(xué)探索的初步跡象已經(jīng)開(kāi)始顯現(xiàn)。
但目前的這些初步嘗試，由于依賴(lài)于計(jì)算量極大的AI模型或需要大量的專(zhuān)家級(jí)人工參與和監(jiān)督，因此難以大規(guī)模推廣。
然而，陶哲軒相信在不遠(yuǎn)的將來(lái)，我們將見(jiàn)證更多創(chuàng)新的機(jī)器輔助數(shù)學(xué)方法的誕生。
參考資料：
https://mathstodon.xyz/@tao/112221953164171331
