|
幾個(gè)世紀(jì)以來(lái)，數(shù)學(xué)家一直依靠計(jì)算機(jī)（人類(lèi)、機(jī)械或電子）和機(jī)器來(lái)協(xié)助他們的研究（如果考慮到算盤(pán)等早期計(jì)算工具，甚至幾千年）。例如，自從納皮爾（John Napier，1550 - 1617）等人的早期對(duì)數(shù)表以來(lái)，數(shù)學(xué)家就知道構(gòu)建數(shù)學(xué)對(duì)象的大型數(shù)據(jù)集來(lái)執(zhí)行計(jì)算和做出猜想的價(jià)值。勒讓德（Adrien-Marie Legendre，1752 - 1833）和高斯（Carl Friedrich Gauss，1777 - 1855）使用人類(lèi)計(jì)算機(jī)編制的大素?cái)?shù)表來(lái)猜想現(xiàn)在所謂的素?cái)?shù)定理（PNT）；一個(gè)半世紀(jì)后，伯奇（Bryan John Birch，1931 -）和斯溫納頓-戴爾（Peter Swinnerton-Dyer，1927 - 2018）同樣使用早期電子計(jì)算機(jī)生成有限域上橢圓曲線(xiàn)的足夠數(shù)據(jù)，以提出他們自己對(duì)這些對(duì)象的著名猜想（即BSD猜想）。毫無(wú)疑問(wèn)，許多讀者已經(jīng)利用了最廣泛的數(shù)學(xué)數(shù)據(jù)集之一——整數(shù)數(shù)列在線(xiàn)百科全書(shū)（OEIS），它產(chǎn)生了無(wú)數(shù)猜想以及在不同數(shù)學(xué)領(lǐng)域之間意想不到的聯(lián)系，并為研究人員提供了一個(gè)有價(jià)值的數(shù)學(xué)對(duì)象的文獻(xiàn)搜索引擎。他們不知道該數(shù)學(xué)對(duì)象的名稱(chēng)，但可以將其與整數(shù)序列相關(guān)聯(lián)。在21世紀(jì)，此類(lèi)大型數(shù)據(jù)庫(kù)還可以作為機(jī)器學(xué)習(xí)算法的關(guān)鍵訓(xùn)練數(shù)據(jù)，這些算法有望實(shí)現(xiàn)自動(dòng)化或者至少大大簡(jiǎn)化數(shù)學(xué)猜想和聯(lián)系的生成過(guò)程。 除了數(shù)據(jù)生成之外，計(jì)算機(jī)的另一個(gè)重要用途是科學(xué)計(jì)算，如今科學(xué)計(jì)算被大量用于數(shù)值求解微分方程和動(dòng)力系統(tǒng)，或計(jì)算大型矩陣或線(xiàn)性算子的統(tǒng)計(jì)數(shù)據(jù)。這種計(jì)算的早期例子出現(xiàn)在1920年代，當(dāng)時(shí)亨德里克·洛倫茲（Hendrik Lorentz，1853 - 1928）組建了一組人類(lèi)計(jì)算機(jī)來(lái)模擬阿夫魯戴克大壩（Afsluitdijk，當(dāng)時(shí)荷蘭正在建設(shè)的一座水壩）周?chē)牧黧w流動(dòng)；除其他外，該計(jì)算因開(kāi)創(chuàng)了現(xiàn)在標(biāo)準(zhǔn)的浮點(diǎn)運(yùn)算裝置而聞名。但現(xiàn)代計(jì)算機(jī)代數(shù)系統(tǒng)（CAS，例如Magma、SAGEMath、Mathematica、Maple等）以及更通用的編程語(yǔ)言可以遠(yuǎn)遠(yuǎn)超出傳統(tǒng)的“數(shù)字運(yùn)算”；它們現(xiàn)在通常用于執(zhí)行代數(shù)、分析、幾何、數(shù)論和許多其他數(shù)學(xué)分支中的符號(hào)計(jì)算。由于舍入誤差和不穩(wěn)定性，某些形式的科學(xué)計(jì)算是眾所周知的不可靠，但人們通?？梢杂酶鼑?yán)格的方法來(lái)代替這些方法（例如，用區(qū)間算術(shù)代替浮點(diǎn)算術(shù)），這可能會(huì)增加運(yùn)行時(shí)間或內(nèi)存使用量。 計(jì)算機(jī)代數(shù)系統(tǒng)的近親是可滿(mǎn)足性（SAT，satisfiability）求解器和可滿(mǎn)足性模理論 (SMT，satisfiability modulo theory) 求解器，它們可以根據(jù)某些受限制的假設(shè)集合對(duì)結(jié)論進(jìn)行復(fù)雜的邏輯推導(dǎo)，并為每個(gè)此類(lèi)推導(dǎo)生成證明證書(shū)。當(dāng)然，可滿(mǎn)足性是一個(gè) NP完全問(wèn)題，因此這些求解器的規(guī)模不會(huì)超過(guò)某個(gè)臨界點(diǎn)。以下是使用SAT求解器證明結(jié)果的典型示例： 定理 0.1 （布爾勾股數(shù)三元組定理【HKM16】） 集合{1, ? ,7824}的元素可以分為兩類(lèi)，使得每一類(lèi)中都不包含勾股數(shù)三元組——滿(mǎn)足a2+b2=c2的(a,b,c)；然而，對(duì)于集合{1, ? ,7825}這是不可能的。 該證明需要4個(gè)CPU年的計(jì)算并生成200TB的命題證明，后來(lái)被壓縮到68GB。 當(dāng)然，數(shù)學(xué)家也經(jīng)常使用計(jì)算機(jī)來(lái)完成日常任務(wù)，例如撰寫(xiě)論文以及與合作者交流。但近幾十年來(lái)，出現(xiàn)了幾種利用計(jì)算機(jī)輔助數(shù)學(xué)研究的有前途的新方法：
這些類(lèi)型的工具中的每一種都已經(jīng)在不同的數(shù)學(xué)領(lǐng)域找到了合適的應(yīng)用，但我發(fā)現(xiàn)特別有趣的是將這些工具組合在一起的可能性，用一種工具抵消另一種工具的弱點(diǎn)。例如，形式證明助手和計(jì)算機(jī)代數(shù)包可以過(guò)濾掉現(xiàn)在臭名昭著的大語(yǔ)言模型看似合理的廢話(huà)的“幻覺(jué)”傾向，而反之，這些模型可以幫助自動(dòng)化證明形式化中更繁瑣的方面，并提供用于運(yùn)行復(fù)雜符號(hào)或機(jī)器學(xué)習(xí)算法的自然語(yǔ)言界面。其中許多組合仍?xún)H處于概念驗(yàn)證開(kāi)發(fā)階段，該技術(shù)需要一定的時(shí)間才能變得成熟起來(lái)成為數(shù)學(xué)家真正有用且可靠的工具。然而，早期的實(shí)驗(yàn)似乎確實(shí)令人鼓舞，我們應(yīng)該期待在不久的將來(lái)會(huì)出現(xiàn)一些令人驚訝的新數(shù)學(xué)研究模式的演示；它不是科幻小說(shuō)中可以自主解決復(fù)雜數(shù)學(xué)問(wèn)題的超級(jí)智能人工智能，而是一個(gè)有價(jià)值的助手，可以提出新想法、過(guò)濾錯(cuò)誤、執(zhí)行例行案例檢查、數(shù)值實(shí)驗(yàn)和文獻(xiàn)評(píng)審任務(wù)，讓人類(lèi)數(shù)學(xué)家能夠在項(xiàng)目中注重對(duì)高層概念的探索。
當(dāng)然，計(jì)算是使用計(jì)算機(jī)執(zhí)行的這一事實(shí)并不能自動(dòng)保證其正確。計(jì)算可能會(huì)產(chǎn)生數(shù)值誤差，例如由于用離散近似值替換連續(xù)變量或方程而引起的誤差。代碼中可能會(huì)無(wú)意中引入錯(cuò)誤，或者輸入數(shù)據(jù)本身可能包含不準(zhǔn)確之處。即使計(jì)算機(jī)用來(lái)運(yùn)行代碼的編譯器也可能存在缺陷。最后，即使代碼完美執(zhí)行，代碼正確計(jì)算的表達(dá)式也可能不是數(shù)學(xué)論證真正想要的表達(dá)式。 早期的計(jì)算機(jī)輔助證明遇到了許多這樣的問(wèn)題。例如，凱尼斯·阿佩爾（Kenneth Appel，1932 - 2013）和沃夫?qū)す希╓olfgang Haken，1928 - 2022）在1976年對(duì)四色定理【AH89】的原始證明圍繞著一系列1834個(gè)需要遵守兩個(gè)性質(zhì)稱(chēng)為“可歸約性”（reducibility）和“不可避免性”（unavoidability）的圖?？梢酝ㄟ^(guò)每次將每個(gè)圖輸入一個(gè)定制的軟件來(lái)檢查可歸約性；但不可避免的是，需要進(jìn)行繁瑣的計(jì)算，包括數(shù)百頁(yè)的縮微膠片——通過(guò)哈肯的女兒Dorothea Blostein（多蘿西婭·布洛斯坦）的英勇努力手工驗(yàn)證——最終包含多個(gè)（可修復(fù)的）錯(cuò)誤。1994年，Robertson、Sanders、Seymour和 Thomas【RSST96】試圖使Appel–Haken證明的計(jì)算部分完全可由計(jì)算機(jī)驗(yàn)證，但最終卻產(chǎn)生了一個(gè)更簡(jiǎn)單的論證（僅涉及633個(gè)圖，以及驗(yàn)證不可避免性的更簡(jiǎn)單的程序），可以通過(guò)用任意數(shù)量的標(biāo)準(zhǔn)編程語(yǔ)言編寫(xiě)的計(jì)算機(jī)代碼更有效地驗(yàn)證。 證明助手將這種形式化更進(jìn)一步，作為一種特殊類(lèi)型的計(jì)算機(jī)語(yǔ)言，其設(shè)計(jì)目的不是執(zhí)行純粹的計(jì)算任務(wù)，而是驗(yàn)證邏輯或數(shù)學(xué)論證結(jié)論的正確性。粗略地說(shuō)，數(shù)學(xué)證明中的每個(gè)步驟都對(duì)應(yīng)于該語(yǔ)言中的多行代碼，并且只有在證明有效的情況下才能編譯整個(gè)代碼?，F(xiàn)代證明助手，例如Coq、Isabelle或Lean，有意嘗試模仿數(shù)學(xué)寫(xiě)作的語(yǔ)言和結(jié)構(gòu)，盡管它們?cè)谠S多方面通常更加挑剔。舉一個(gè)簡(jiǎn)單的例子，為了解釋一個(gè)數(shù)學(xué)表達(dá)式，例如a?,形式的證明助手可能需要精確指定基礎(chǔ)變量a,b的“類(lèi)型”（例如，自然數(shù)、實(shí)數(shù)、復(fù)數(shù)），以便確定正在使用哪種求冪運(yùn)算（這對(duì)于諸如0?的表達(dá)式尤其重要，在不同的求冪概念下，其解釋略有不同）。人們投入了大量精力來(lái)開(kāi)發(fā)自動(dòng)化工具和廣泛的數(shù)學(xué)結(jié)果庫(kù)來(lái)管理形式證明的這些低級(jí)方面，但在實(shí)踐中，數(shù)學(xué)論證的“明顯”部分通常比“重要”部分需要更長(zhǎng)的時(shí)間才能形式化。舉一個(gè)例子：給定三個(gè)集合A?,A?,A?，數(shù)學(xué)家可能會(huì)相互切換使用笛卡爾積(A?×A?)×A?, A?×(A?×A?)和∏_{i∈{1,2,3}}A?，因?yàn)樗鼈儭帮@然”是“同一”對(duì)象；但在大多數(shù)數(shù)學(xué)形式化中，這些乘積實(shí)際上并不相同，并且論證的形式化版本可能需要投入一部分證明來(lái)在這些空間之間建立適當(dāng)?shù)牡葍r(jià)性，并確保涉及該乘積的一個(gè)版本的陳述對(duì)于另一個(gè)版本繼續(xù)成立。 由于這個(gè)和其它的原因，將人類(lèi)數(shù)學(xué)家（即使是非常仔細(xì)的數(shù)學(xué)家）編寫(xiě)的證明轉(zhuǎn)換為在形式證明助手中編譯的形式證明的任務(wù)相當(dāng)耗時(shí)，盡管隨著時(shí)間的推移，這個(gè)過(guò)程逐漸變得更加高效。上述四色定理由Werner和Gonthier于2005年【Gon08】在Coq中形式化。關(guān)于??3中對(duì)單位球最密堆積的臭名昭著的開(kāi)普勒猜想的證明由Hales和Ferguson在1998年【Hal05】的一個(gè)非常復(fù)雜的（計(jì)算機(jī)輔助的）證明中證明。2003年，Hales啟動(dòng)了Flyspeck項(xiàng)目來(lái)形式化地驗(yàn)證證明，預(yù)計(jì)需要20年才能完成，盡管最終通過(guò)Hales和其他21位貢獻(xiàn)者的合作，“僅”用了11年就實(shí)現(xiàn)了這一目標(biāo)【HAB?17】。最近，舒爾茨（Peter Scholze，1987 -）于2019年啟動(dòng)了“液體張量實(shí)驗(yàn)” 【Com22】，形式驗(yàn)證了他和克勞森（Dustin Clausen）關(guān)于凝聚態(tài)數(shù)學(xué)理論中“液體向量空間”的某個(gè)Ext群消失的基本定理。人類(lèi)寫(xiě)的證明“只有”十頁(yè)長(zhǎng)，盡管包含大量凝聚態(tài)數(shù)學(xué)的先決材料；盡管如此，通過(guò)大量的協(xié)作努力，Lean的形式化花費(fèi)了大約18個(gè)月的時(shí)間。我本人領(lǐng)導(dǎo)了一項(xiàng)關(guān)于高爾斯、格林、曼納斯和我自己的加性組合猜想【GGMT23】最近證明的形式化工作【Tao23】；人工編寫(xiě)的證明長(zhǎng)達(dá)33頁(yè)，但基本上是自給自足的，大約20名合作者組成的小組在三周內(nèi)將其形式化。有些數(shù)學(xué)領(lǐng)域比其他領(lǐng)域更難以形式化；凱文·巴扎德（Kevin Buzzard，1968 -）最近宣布了一項(xiàng)形式化費(fèi)馬大定理證明的項(xiàng)目，他估計(jì)至少需要五年時(shí)間完成。 考慮到所需的所有努力，數(shù)學(xué)證明的形式化工作對(duì)數(shù)學(xué)的價(jià)值是什么？最明顯的是，它為給定結(jié)果的正確性提供了極高的置信度，這對(duì)于有爭(zhēng)議或因強(qiáng)烈吸引虛假證明而臭名昭著的結(jié)果特別有價(jià)值，或者對(duì)于審閱人愿意逐行驗(yàn)證此類(lèi)特別冗長(zhǎng)的證明的領(lǐng)域尤其供不應(yīng)求。（理論上，證明助手編譯器中仍然可能存在隱藏的缺陷 - 故意將其保持得盡可能小以減少這種可能性 - 或者結(jié)果的形式聲明中使用的定義可能在微妙但重要的方面與人類(lèi)可讀的陳述有所不同，但這種情況不太可能發(fā)生，特別是如果形式證明密切跟蹤人類(lèi)編寫(xiě)的證明的前提下。）形式化過(guò)程通常會(huì)發(fā)現(xiàn)人類(lèi)證明中的小問(wèn)題，有時(shí)可以揭示論證的簡(jiǎn)化或強(qiáng)化，例如通過(guò)揭示一個(gè)看似重要的假設(shè)在引理中實(shí)際上是不必要的，或者可以使用低功效但更通用的工具來(lái)代替高級(jí)但專(zhuān)門(mén)的工具。采用現(xiàn)代語(yǔ)言（例如Lean）的形式化項(xiàng)目通常會(huì)將項(xiàng)目過(guò)程中生成的許多基本數(shù)學(xué)結(jié)果貢獻(xiàn)到公共數(shù)學(xué)庫(kù)中，這使得未來(lái)形式化項(xiàng)目更容易進(jìn)行。 但形式證明助手也可以實(shí)現(xiàn)數(shù)學(xué)教育和協(xié)作的新模式。幾個(gè)實(shí)驗(yàn)項(xiàng)目正在進(jìn)行中，以獲取形式證明并將其轉(zhuǎn)換為更易于人類(lèi)理解的形式，例如一段交互式文本，其中論證中的各個(gè)步驟可以擴(kuò)展為更詳細(xì)的內(nèi)容或折疊為高級(jí)摘要；這可能是一種特別適合未來(lái)數(shù)學(xué)教科書(shū)的格式。傳統(tǒng)的數(shù)學(xué)合作很少涉及超過(guò)五個(gè)左右的共同作者，部分原因是每個(gè)共同作者都需要信任和驗(yàn)證其他人的工作；但形式化項(xiàng)目通常會(huì)涉及數(shù)十名之前沒(méi)有互動(dòng)過(guò)的人，這正是因?yàn)樾问阶C明助手允許項(xiàng)目中的各個(gè)子任務(wù)獨(dú)立于其他子任務(wù)進(jìn)行精確定義和驗(yàn)證?？梢韵胂螅@些證明助手還可以允許類(lèi)似的分工來(lái)生成新的數(shù)學(xué)結(jié)果，從而允許比以前的在線(xiàn)協(xié)作（例如“Polymath”項(xiàng)目【Gow10】，其規(guī)模由于需要對(duì)討論進(jìn)行人工審核而受到限制）規(guī)模大得多的高度并行和眾包協(xié)作。隨著時(shí)間的推移，其他科學(xué)或軟件工程項(xiàng)目中已經(jīng)建立的大型合作也可能在研究數(shù)學(xué)中變得司空見(jiàn)慣。一些貢獻(xiàn)者可能扮演“項(xiàng)目經(jīng)理”的角色，例如專(zhuān)注于建立精確的“藍(lán)圖”，將項(xiàng)目分解為更小的部分，而其他貢獻(xiàn)者則可以專(zhuān)門(mén)研究項(xiàng)目的各個(gè)組成部分，而不必具備理解整個(gè)項(xiàng)目所需的所有專(zhuān)業(yè)知識(shí)。 然而，在此之前，形式化過(guò)程需要變得更加高效。“de Bruijn因子”（編寫(xiě)正確的形式證明與正確的非形式證明的難度之間的比率）仍然遠(yuǎn)高于1（我估計(jì)約為20)，但在下降中。我相信將該比率降至1以下不存在根本障礙，尤其是因?yàn)锳I、SMT求解器和其他工具的集成度不斷提高；這將給我們的領(lǐng)域帶來(lái)變革。
機(jī)器學(xué)習(xí)是指訓(xùn)練計(jì)算機(jī)執(zhí)行復(fù)雜任務(wù)的一系列技術(shù)，例如預(yù)測(cè)與來(lái)自非常廣泛的類(lèi)別的給定輸入相對(duì)應(yīng)的輸出，或者辨別數(shù)據(jù)集中的相關(guān)性和其他關(guān)系。許多流行的機(jī)器學(xué)習(xí)模型使用某種形式的神經(jīng)網(wǎng)絡(luò)來(lái)編碼計(jì)算機(jī)如何執(zhí)行任務(wù)。這些網(wǎng)絡(luò)是由大量簡(jiǎn)單運(yùn)算（線(xiàn)性和非線(xiàn)性）組合在一起形成的許多變量的函數(shù)；通常，人們會(huì)為這樣的網(wǎng)絡(luò)分配某種獎(jiǎng)勵(lì)函數(shù)（或損失函數(shù)），例如通過(guò)根據(jù)訓(xùn)練數(shù)據(jù)集憑經(jīng)驗(yàn)測(cè)量其性能，然后執(zhí)行計(jì)算密集型優(yōu)化以找到該網(wǎng)絡(luò)的參數(shù)選擇使得獎(jiǎng)勵(lì)函數(shù)盡可能大（或損失函數(shù)盡可能?。?。這些模型具有無(wú)數(shù)的實(shí)際應(yīng)用，例如圖像和語(yǔ)音識(shí)別、推薦系統(tǒng)或欺詐檢測(cè)。然而，它們通常不能提供強(qiáng)有力的準(zhǔn)確性保證，特別是當(dāng)應(yīng)用于與訓(xùn)練數(shù)據(jù)集顯著不同的輸入時(shí)，或者當(dāng)訓(xùn)練數(shù)據(jù)集有噪聲或不完整時(shí)。此外，模型通常是不透明的，因?yàn)楹茈y從模型中提取人類(lèi)可以理解的解釋來(lái)說(shuō)明模型為什么做出特定的預(yù)測(cè)，或者理解模型的一般行為。因此，這些工具乍一看似乎不適合研究數(shù)學(xué)，因?yàn)槿藗兗认Ｍ玫絿?yán)格的證明，又希望對(duì)論證有直觀的理解。 盡管如此，最近出現(xiàn)了一些有前景的用例，即適當(dāng)選擇的機(jī)器學(xué)習(xí)工具可以產(chǎn)生或至少提出新的嚴(yán)格數(shù)學(xué)，特別是與其他可以驗(yàn)證這些工具輸出的更可靠技術(shù)相結(jié)合時(shí)。例如，流體方程數(shù)學(xué)理論（例如歐拉方程或納維-斯托克斯N-S方程）的一個(gè)基本問(wèn)題是能夠嚴(yán)格證明解u在有限時(shí)間內(nèi)從光滑的初始數(shù)據(jù)開(kāi)始有限時(shí)間內(nèi)爆破。最臭名昭著的例子涉及三維不可壓縮納維-斯托克斯方程，該方程的解是（未解決的）千禧年獎(jiǎng)問(wèn)題之一；這仍然遙不可及，但最近在其他流體方程方面取得了進(jìn)展，例如二維的Boussinesq方程（三維不可壓縮歐拉方程的簡(jiǎn)化模型）。建立這種奇點(diǎn)（singularity）的一種途徑是構(gòu)建自相似的爆破解u，由解出一個(gè)更簡(jiǎn)單的偏微分方程（PDE）的低維函數(shù)U描述。該偏微分方程的封閉形式解似乎不可用；但如果能夠產(chǎn)生這個(gè)偏微分方程的足夠高質(zhì)量的近似解?（近似服從某些邊界條件），可以通過(guò)應(yīng)用微擾理論嚴(yán)格證明精確解U（例如基于不動(dòng)點(diǎn)定理的理論）。傳統(tǒng)上，人們會(huì)使用數(shù)值PDE方法來(lái)嘗試產(chǎn)生這些近似解?，例如，通過(guò)將偏微分方程離散化為差分方程（difference equation），但使用此類(lèi)方法獲得具有所需精度水平的解的計(jì)算成本可能很高。Wang、Lai、Gómez-Serrano和Buckmaster【W(wǎng)LGSB23】于2019年提出了另一種方法，他們使用經(jīng)過(guò)訓(xùn)練的物理信息神經(jīng)網(wǎng)絡(luò)（PINN，Physics Informed Neural Network）來(lái)生成函數(shù)?，可以最小化一個(gè)合適的損失函數(shù)，該函數(shù)度量了近似遵守所需偏微分方程和邊界條件的程度。由于這些函數(shù)?通過(guò)神經(jīng)網(wǎng)絡(luò)而不是方程的離散版本生成，它們可以更快地生成，并且可能不易受到數(shù)值不穩(wěn)定的影響。事實(shí)證明，Chen和Hou的同期工作【CH22】能夠使用更傳統(tǒng)的數(shù)值方法為該方程建立有限時(shí)間爆破解；然而，機(jī)器學(xué)習(xí)范式顯示出作為此類(lèi)偏微分方程問(wèn)題的補(bǔ)充方法的巨大潛力。例如，我們可以設(shè)想一種混合方法，其中人類(lèi)數(shù)學(xué)家首先提出一個(gè)爆破模擬，然后神經(jīng)網(wǎng)絡(luò)嘗試找到一個(gè)粗略的近似解，然后使用更傳統(tǒng)的數(shù)值方法將該解細(xì)化得足夠準(zhǔn)確，使得可以對(duì)其應(yīng)用嚴(yán)格的穩(wěn)定性分析。 機(jī)器學(xué)習(xí)在數(shù)學(xué)中應(yīng)用的另一個(gè)例子是紐結(jié)理論（knot theory）領(lǐng)域。結(jié)具有極其多樣化的拓?fù)洳蛔兞浚航Y(jié)的符號(hào)差（signature）是與以結(jié)為邊界的表面（Siefert曲面）的同調(diào)性相關(guān)的整數(shù)；結(jié)的Jones瓊斯多項(xiàng)式可以使用辮子（braid）的表示理論來(lái)描述；大多數(shù)結(jié)（不包括環(huán)面結(jié)torus knot）其補(bǔ)（complement）具有典范雙曲幾何，可用于描述許多雙曲不變量，例如雙曲體積等等。先驗(yàn)地，這些來(lái)自不同數(shù)學(xué)領(lǐng)域的不變量之間的相互關(guān)系并不明顯。然而，2021年，Davies、Juhász、Lackenby和Tomasev【DJLT21】通過(guò)機(jī)器學(xué)習(xí)研究了這個(gè)問(wèn)題。通過(guò)在現(xiàn)有的近200萬(wàn)個(gè)結(jié)（加上100萬(wàn)個(gè)隨機(jī)生成的額外的結(jié)）的數(shù)據(jù)庫(kù)上訓(xùn)練神經(jīng)網(wǎng)絡(luò)，他們能夠使該神經(jīng)網(wǎng)絡(luò)模型從大約兩打雙曲不變量中高精度地預(yù)測(cè)結(jié)的符號(hào)差。然而，生成的預(yù)測(cè)函數(shù)非常不透明，并且最初并沒(méi)有揭示出關(guān)于符號(hào)差和雙曲不變量之間的精確關(guān)系的更多見(jiàn)解。然而，可以通過(guò)一種稱(chēng)為顯著性分析（saliency analysis）的簡(jiǎn)單工具進(jìn)一步進(jìn)行，粗略地說(shuō)，該工具測(cè)量每個(gè)單獨(dú)的雙曲不變量對(duì)預(yù)測(cè)函數(shù)的影響。該分析表明，在使用的兩打雙曲不變量中，只有其中三個(gè)（縱向平移以及子午平移的實(shí)部和復(fù)數(shù)部分）對(duì)預(yù)測(cè)函數(shù)有顯著影響。通過(guò)視覺(jué)上檢查這三個(gè)不變量的符號(hào)差散點(diǎn)圖，作者能夠推測(cè)出這些數(shù)量之間更容易理解的關(guān)系。進(jìn)一步的數(shù)值反駁了他們最初的猜想，但提出了他們能夠嚴(yán)格證明的猜想的修改版本。機(jī)器生成的猜想與人類(lèi)使用理論進(jìn)行驗(yàn)證（和修改）之間的相互作用是一個(gè)有前途的范式，似乎適用于許多其他數(shù)學(xué)領(lǐng)域。 機(jī)器學(xué)習(xí)的許多應(yīng)用需要大量的訓(xùn)練數(shù)據(jù)，理想情況下以某種標(biāo)準(zhǔn)化格式（例如數(shù)字向量）表示，以便現(xiàn)有的機(jī)器學(xué)習(xí)算法可以相對(duì)輕松地應(yīng)用于其中。數(shù)據(jù)的精確表示至關(guān)重要；機(jī)器學(xué)習(xí)算法可以很容易地在一種數(shù)據(jù)表示中發(fā)現(xiàn)數(shù)據(jù)不同組成部分之間的相關(guān)性，但在另一種數(shù)據(jù)表示中幾乎不可能找到。雖然數(shù)學(xué)的一些領(lǐng)域開(kāi)始編制有用對(duì)象的大型數(shù)據(jù)庫(kù)（例如，結(jié)、圖或橢圓曲線(xiàn)），但仍然有許多重要類(lèi)別的更模糊定義的數(shù)學(xué)概念尚未系統(tǒng)地放入可用于機(jī)器學(xué)習(xí)的形式中。例如，回到偏微分方程的例子，文獻(xiàn)中研究了數(shù)千種不同的偏微分方程，但通常在符號(hào)和項(xiàng)的代數(shù)排列方面具有很大的可變性，而且沒(méi)有什么類(lèi)似于通常所研究的偏微分方程的標(biāo)準(zhǔn)數(shù)據(jù)庫(kù)（例如，研究它們是橢圓形、拋物線(xiàn)形還是雙曲形；解的存在性和唯一性、守恒定律等已知的信息）。這樣的數(shù)據(jù)庫(kù)可能有助于根據(jù)其他偏微分方程的結(jié)果對(duì)一個(gè)偏微分方程的行為進(jìn)行推測(cè)性預(yù)測(cè)，或者建議從一種偏微分方程到另一種偏微分方程的可能類(lèi)比或化簡(jiǎn)；但由于缺乏任何規(guī)范范式來(lái)表示此類(lèi)方程（或至少缺乏識(shí)別它們的“指紋” 【BT13】），因此目前構(gòu)建這樣的數(shù)據(jù)庫(kù)都非常困難，更不用說(shuō)將其輸入神經(jīng)網(wǎng)絡(luò)了。可以想象，未來(lái)的證明形式化和人工智能的進(jìn)步可能會(huì)使生成和利用此類(lèi)數(shù)據(jù)庫(kù)（可能包含“真實(shí)世界”和“合成”數(shù)據(jù)集）變得更加可行。
大語(yǔ)言模型（LLM）是一種相對(duì)較新的機(jī)器學(xué)習(xí)模型，適合對(duì)極其廣泛和大型的自然語(yǔ)言文本數(shù)據(jù)集進(jìn)行訓(xùn)練。一種流行的大語(yǔ)言模型是GPT（Generative Pre-trained Transformer生成式預(yù)訓(xùn)練轉(zhuǎn)換器），顧名思義，它是圍繞Transformer模型（一種神經(jīng)網(wǎng)絡(luò)變體，旨在預(yù)測(cè)字符串中的下一個(gè)單詞即“token詞元”，并保留對(duì)字符串早期單詞的一些長(zhǎng)期“注意力”，以模擬句子的上下文）構(gòu)建的。通過(guò)迭代該模型，人們可以對(duì)給定的文本提示（prompt）生成冗長(zhǎng)的文本響應(yīng)。當(dāng)使用少量數(shù)據(jù)進(jìn)行訓(xùn)練時(shí)，此類(lèi)模型的輸出并不令人印象深刻，例如，并不比嘗試在智能手機(jī)上迭代“自動(dòng)完成”文本輸入功能復(fù)雜多少，但經(jīng)過(guò)對(duì)極大且多樣化的數(shù)據(jù)集進(jìn)行大量訓(xùn)練后，這些模型的輸出可以令人驚訝地連貫，甚至具有創(chuàng)造性，并且可以生成乍一看很難與人類(lèi)書(shū)寫(xiě)區(qū)分開(kāi)的文本，盡管仔細(xì)檢查后，輸出通常是無(wú)意義的，并且與任何基本事實(shí)沒(méi)有聯(lián)系，這種現(xiàn)象被認(rèn)為是“幻覺(jué)”（hallucination）。 人們當(dāng)然可以嘗試應(yīng)用這種通用的LLM來(lái)嘗試直接解決數(shù)學(xué)問(wèn)題。有時(shí)，結(jié)果可能相當(dāng)令人印象深刻；例如布貝克（Bubeck）等人記錄了一個(gè)案例，其中強(qiáng)大的大語(yǔ)言模型GPT-4能夠提供2022年國(guó)際數(shù)學(xué)奧林匹克問(wèn)題的完整且正確的證明，該問(wèn)題并不在該模型的訓(xùn)練數(shù)據(jù)集中。相反，該模型不太適合執(zhí)行精確計(jì)算，甚至基本算術(shù)；在一個(gè)例子【BCE?23】中，當(dāng)要求計(jì)算表達(dá)式7×4 + 8×8時(shí)，GPT-4立即給出了錯(cuò)誤答案120，然后繼續(xù)通過(guò)分步過(guò)程來(lái)證明計(jì)算的合理性返回正確答案92。當(dāng)被問(wèn)及這一差異時(shí)，GPT-4只表示其最初的猜測(cè)是一個(gè)“拼寫(xiě)錯(cuò)誤”（typo）。這些問(wèn)題可以通過(guò)使用GPT-4的“插件”得到一定程度的補(bǔ)償，其中GPT-4被訓(xùn)練為向外部工具（例如Wolfram Alpha）發(fā)送特定類(lèi)型的查詢(xún)（例如數(shù)學(xué)計(jì)算），而不是通過(guò)其內(nèi)部模型猜測(cè)答案，盡管目前工具之間的集成還不是無(wú)縫的。類(lèi)似地，最近的概念驗(yàn)證【RPBN?23】已經(jīng)表明，LLM可用于查找組合學(xué)和計(jì)算機(jī)科學(xué)中各種問(wèn)題的示例，這些示例優(yōu)于以前的人類(lèi)生成的示例，方法是要求這些模型生成程序來(lái)創(chuàng)建此類(lèi)示例，而不是嘗試直接構(gòu)建示例，然后使用另一種語(yǔ)言執(zhí)行該程序來(lái)可靠地驗(yàn)證輸出的質(zhì)量，然后將其發(fā)送回原始模型以提示其對(duì)猜測(cè)進(jìn)行改進(jìn)。最近在使用LLM來(lái)增強(qiáng)現(xiàn)有符號(hào)證明引擎以解決狹窄類(lèi)別的數(shù)學(xué)問(wèn)題（例如奧林匹克幾何問(wèn)題【TWL?24】）方面也取得了進(jìn)展. 在我自己的GPT-4實(shí)驗(yàn)中（可以在 https://terrytao./mastodon-posts/ 找到），我發(fā)現(xiàn)最高效的用例是生成各種語(yǔ)言的基本計(jì)算機(jī)代碼（Python、SAGE、LaTeX、Lean、正則表達(dá)式等），或者清理凌亂且無(wú)組織的數(shù)據(jù)集（例如，在起初提供GPT-4一些所需參考書(shū)目條目格式的示例后，讓它將互聯(lián)網(wǎng)上抓取的一堆參考文獻(xiàn)整理成連貫的LaTeX參考書(shū)目）。在這種情況下，它通常會(huì)在第一次嘗試時(shí)產(chǎn)生令人滿(mǎn)意或接近令人滿(mǎn)意的輸出，只需進(jìn)行少量修改即可獲得我正在尋求的輸出類(lèi)型。我在讓GPT-4為實(shí)際數(shù)學(xué)問(wèn)題推薦相關(guān)文獻(xiàn)或技術(shù)方面也取得了一些有限的成功。在一個(gè)測(cè)試用例中，我問(wèn)它如何計(jì)算獨(dú)立隨機(jī)變量之和的尾部概率的指數(shù)衰減率，以在不給它提供大偏差理論（large deviation theory）等關(guān)鍵詞前提下，評(píng)估它是否知道這方面的相關(guān)定理（Cramér定理）。事實(shí)證明，GPT-4并沒(méi)有準(zhǔn)確定位這個(gè)定理，而是產(chǎn)生了一串?dāng)?shù)學(xué)廢話(huà)，但奇怪的是，它確實(shí)引用了對(duì)數(shù)矩生成函數(shù)（logarithmic moment generating function），這是Cramér定理陳述中的一個(gè)關(guān)鍵概念，即使它似乎并不確切地“知道”這個(gè)函數(shù)與問(wèn)題的相關(guān)性。在另一個(gè)實(shí)驗(yàn)中，我向GPT-4詢(xún)問(wèn)如何證明我正在研究的組合恒等式的建議。它給出了一些我已經(jīng)考慮過(guò)的建議（漸近分析、歸納、數(shù)值）以及一些通用建議（簡(jiǎn)化表達(dá)式、尋找類(lèi)似問(wèn)題、理解問(wèn)題），而且還提出了一種技術(shù)（生成函數(shù)）我只是忽略了這一點(diǎn)，最終很容易地解決了這個(gè)問(wèn)題。另一方面，這樣的建議列表對(duì)于新手?jǐn)?shù)學(xué)家來(lái)說(shuō)可能沒(méi)什么用，因?yàn)樗麄儧](méi)有足夠的經(jīng)驗(yàn)來(lái)獨(dú)立評(píng)估每個(gè)建議的有用性。盡管如此，我看到這些工具在提取用戶(hù)對(duì)一個(gè)問(wèn)題的潛在知識(shí)方面的作用，只需成為一個(gè)好的傾聽(tīng)者并提出足夠用戶(hù)給出專(zhuān)業(yè)評(píng)估的合理相關(guān)的想法即可。 Github Copilot（副駕駛）是另一個(gè)GPT模型，已集成到多個(gè)流行的代碼編輯器中。它經(jīng)過(guò)不同語(yǔ)言的大型代碼數(shù)據(jù)集的訓(xùn)練，旨在利用上下文線(xiàn)索（例如代碼中其他地方要執(zhí)行的任務(wù)的非形式描述）為部分編寫(xiě)的代碼提供自動(dòng)完成建議。我發(fā)現(xiàn)它對(duì)于編寫(xiě)數(shù)學(xué)LaTeX以及在Lean中形式化非常有效；事實(shí)上，它在我寫(xiě)作時(shí)建議了幾句話(huà)，從而幫助我寫(xiě)了這篇文章，其中許多句子我在最終版本中保留著或進(jìn)行了輕微編輯。雖然其建議的質(zhì)量差異很大，但有時(shí)它可以表現(xiàn)出對(duì)文本意圖的模擬理解的不可思議的水平。例如，在編寫(xiě)另一篇關(guān)于如何估計(jì)積分的闡述性L(fǎng)aTeX筆記時(shí)，我描述了如何將積分分解為三個(gè)部分，然后詳細(xì)說(shuō)明了如何估計(jì)第一部分。然后Copilot立即建議如何通過(guò)類(lèi)似的方法來(lái)估計(jì)第二部分，并以完全正確的方式改變變量。這些頻繁經(jīng)歷使我在LaTeX和Lean的寫(xiě)作中獲得了小幅但明顯的加速，我預(yù)計(jì)這些工具在未來(lái)會(huì)變得更加有用，因?yàn)榭梢愿鶕?jù)個(gè)人寫(xiě)作風(fēng)格和喜好“微調(diào)”這些模型。
上面討論的各種技術(shù)都有非常不同的優(yōu)點(diǎn)和缺點(diǎn)，而且就其目前的發(fā)展水平而言，沒(méi)有一種技術(shù)適合作為數(shù)學(xué)家的通用工具，能與LaTeX或arXiv等無(wú)處不在的平臺(tái)相媲美。然而，最近有一些有希望的實(shí)驗(yàn)可以通過(guò)將兩種或多種單獨(dú)的技術(shù)結(jié)合在一起來(lái)創(chuàng)建更令人滿(mǎn)意的工具。例如，在生成證明時(shí)對(duì)抗LLM的幻覺(jué)性質(zhì)的一種可行方法是要求模型以形式證明助手的語(yǔ)言格式化其輸出，并將助手生成的任何錯(cuò)誤作為反饋發(fā)送回模型。這個(gè)組合系統(tǒng)似乎適合生成簡(jiǎn)單命題的簡(jiǎn)短證明【YSG?23】；由于此類(lèi)任務(wù)通常是有效形式化證明的限制因素，因此這種范式可以大大加快這種形式化的速度，特別是如果這些模型在形式化證明（而不是一般文本）上進(jìn)行微調(diào)，并與更傳統(tǒng)的自動(dòng)化定理證明方法集成，例如SMT求解器的部署。 由于能夠接受自然語(yǔ)言輸入，LLM還可能是一個(gè)用戶(hù)友好的界面，允許沒(méi)有特定軟件專(zhuān)業(yè)知識(shí)的數(shù)學(xué)家使用高級(jí)工具。如前所述，我和許多其他人已經(jīng)經(jīng)常使用此類(lèi)模型來(lái)生成各種語(yǔ)言的簡(jiǎn)單代碼（包括符號(hào)代數(shù)包），或創(chuàng)建復(fù)雜的圖表和圖像；似乎可以合理地預(yù)期，在不久的將來(lái)，人們還可以通過(guò)此類(lèi)模型進(jìn)行通信，僅使用高級(jí)會(huì)話(huà)指令來(lái)設(shè)計(jì)和操作像機(jī)器學(xué)習(xí)模型這樣復(fù)雜的東西。更雄心勃勃的是，人們可能希望最終能夠通過(guò)用自然語(yǔ)言向人工智能解釋結(jié)果來(lái)生成完整的研究論文（初稿），并完成形式驗(yàn)證，人工智能將嘗試形式化結(jié)果的每一步并在需要澄清時(shí)詢(xún)問(wèn)作者。 當(dāng)前形式的形式化證明驗(yàn)證的人力密集性質(zhì)意味著當(dāng)前研究論文的很大一部分實(shí)時(shí)完全形式化是不可行的。然而，許多已經(jīng)用于驗(yàn)證研究論文中特定計(jì)算密集型部分的工具（例如數(shù)值積分或 PDE求解器、符號(hào)代數(shù)計(jì)算或使用SMT求解器建立的結(jié)果）似乎可以進(jìn)行修改之后出具形式證明證書(shū)。此外，可以以這種方式形式化的計(jì)算類(lèi)別可以從當(dāng)前實(shí)踐中大大擴(kuò)展。僅舉一個(gè)例子，在偏微分方程領(lǐng)域，通常會(huì)使用大量計(jì)算來(lái)估計(jì)涉及一個(gè)或多個(gè)未知函數(shù)（例如一個(gè)偏微分方程的解）的某些積分表達(dá)式，并使用各種函數(shù)空間范數(shù)中此類(lèi)函數(shù)的界限（例如Sobolev索博列夫空間范數(shù)），以及標(biāo)準(zhǔn)不等式（例如，H?lder霍爾德不等式和Sobolev索博列夫不等式），以及各種恒等式，例如分部積分或積分符號(hào)下的微分。此類(lèi)計(jì)算雖然是常規(guī)計(jì)算，但可能包含不同嚴(yán)重程度的拼寫(xiě)錯(cuò)誤（例如符號(hào)錯(cuò)誤），并且仔細(xì)審閱可能會(huì)很乏味，因?yàn)橛?jì)算本身除了驗(yàn)證最終估計(jì)值是否成立之外幾乎沒(méi)有提供任何見(jiàn)解?？梢韵胂螅梢蚤_(kāi)發(fā)工具來(lái)以自動(dòng)或半自動(dòng)的方式建立此類(lèi)估計(jì)，并且當(dāng)前此類(lèi)估計(jì)的冗長(zhǎng)且無(wú)啟發(fā)性的證明可以由形式證明證書(shū)的鏈接取代。更雄心勃勃的是，人們可能能夠要求未來(lái)的AI人工智能工具在給定一組初始假設(shè)和方法的情況下產(chǎn)生最佳估計(jì)，而無(wú)需首先進(jìn)行一些紙筆計(jì)算來(lái)猜測(cè)估計(jì)值是什么。目前，可能估計(jì)的狀態(tài)空間太復(fù)雜，無(wú)法以這種方式自動(dòng)探索；但我認(rèn)為隨著技術(shù)的進(jìn)步，這種自動(dòng)化沒(méi)有理由無(wú)法實(shí)現(xiàn)。當(dāng)這種情況成為現(xiàn)實(shí)時(shí)，目前尚不可行的大規(guī)模的數(shù)學(xué)探索就成為可能。繼續(xù)以偏微分方程為例，該領(lǐng)域的論文通常一次研究一兩個(gè)方程；但在未來(lái)，人們可能能夠同時(shí)研究數(shù)百個(gè)方程，也許只為一個(gè)方程給出完整的論證，然后讓人工智能工具將論證適應(yīng)一大族的相關(guān)方程，在推廣的論點(diǎn)非常規(guī)時(shí)詢(xún)問(wèn)作者是否有必要擴(kuò)展。這種大規(guī)模數(shù)學(xué)探索的一些提示開(kāi)始在數(shù)學(xué)的其他領(lǐng)域出現(xiàn)，例如圖論中猜想的自動(dòng)探索【W(wǎng)ag21】。 目前尚不清楚這些實(shí)驗(yàn)中哪一個(gè)最終將最成功地為典型的數(shù)學(xué)家?guī)?lái)先進(jìn)的計(jì)算機(jī)輔助。一些概念證明目前無(wú)法擴(kuò)展，特別是那些依賴(lài)于計(jì)算極其密集（且通常是專(zhuān)有）的人工智能模型，或需要大量專(zhuān)家人工輸入和監(jiān)督的證明。然而，我對(duì)探索可能性空間的各種努力感到鼓舞，并相信在不久的將來(lái)會(huì)有更多執(zhí)行機(jī)器輔助數(shù)學(xué)的新方法的例子。
機(jī)器輔助證明的主題相當(dāng)廣泛，分布在數(shù)學(xué)、計(jì)算機(jī)科學(xué)甚至工程學(xué)的各個(gè)領(lǐng)域；雖然每個(gè)單獨(dú)的子領(lǐng)域都有大量的活動(dòng)，但直到最近才努力建立一個(gè)更加統(tǒng)一的社區(qū)，將此處列出的所有主題匯集在一起。因此，目前很少有地方可以找到對(duì)這些快速發(fā)展的數(shù)學(xué)模式的全面調(diào)查。一個(gè)起點(diǎn)是2023年6月美國(guó)國(guó)家科學(xué)院“人工智能輔助數(shù)學(xué)推理”研討會(huì)的會(huì)議記錄【Kor23】（作者是該研討會(huì)的聯(lián)合組織者之一）；作為該研討會(huì)的成果之一，Talia Ringer領(lǐng)導(dǎo)了一項(xiàng)為數(shù)學(xué)資源編譯AI的工作，其結(jié)果可以在https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0 中找到。
例如，該文檔中有一個(gè)指向“自然數(shù)字游戲”的鏈接，這是一種開(kāi)始熟悉Lean證明輔助語(yǔ)言的易于訪(fǎng)問(wèn)和交互的方式。這里討論的許多例子也取自2023年2月的IPAM研討會(huì)“機(jī)器輔助證明”（作者也參與共同組織），該研討會(huì)的演講可以在網(wǎng)上找到。 感謝匿名審稿人的指正和建議。
[AH89] Kenneth Appel and Wolfgang Haken, Every planar map is four colorable, Contemporary Mathematics, vol. 98, American Mathematical Society, Providence, RI, 1989. With the collaboration of J. Koch, DOI 10.1090/conm/098. MR1025335 [BT13] Sara C. Billey and Bridget E. Tenner, Fingerprint databases for theorems, Notices Amer. Math. Soc. 60 (2013), no. 8, 1034–1039, DOI 10.1090/noti1029. MR3113227 [BCE?23] Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang, Sparks of artificial general intelligence: Early experiments with GPT-4, Preprint, arXiv:2303.12712, 2023. [CH22] Jiajie Chen and Thomas Y. Hou, Stable nearly self-similar blowup of the 2D Boussinesq and 3D Euler equations with smooth data, parts I and II, 2022. arXiv:2210.07191; arXiv:2305.05660. [Com22] Johan Commelin, Liquid tensor experiment (German, with German summary), Mitt. Dtsch. Math.-Ver. 30 (2022), no. 3, 166–170, DOI 10.1515/dmvm-2022-0058. MR4469845 [DJLT21] Alex Davies, András Juhász, Marc Lackenby, and Nenad Tomasev, The signature and cusp geometry of hyperbolic knots, Preprint, arXiv:2111.15323, 2021. [Gon08] Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR2463991 [Gow10] W. T. Gowers, Polymath and the density Hales-Jewett theorem, An irregular mind, Bolyai Soc. Math. Stud., vol. 21, János Bolyai Math. Soc., Budapest, 2010, pp. 659–687, DOI 10.1007/978-3-642-14444-8_21. MR2815619 [GGMT23] W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao, On a conjecture of Marton, Preprint, arXiv:2311.05762, 2023. [HAB?17] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2, 29, DOI 10.1017/fmp.2017.1. MR3659768 [Hal05] Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185, DOI 10.4007/annals.2005.162.1065. MR2179728 [HKM16] Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, Theory and applications of satisfiability testing—SAT 2016, 2016, pp. 228–245, DOI 10.1007/978-3-319-40970-2_15. MR3534782 [Kor23] Samantha Koretsky (ed.), Artificial intelligence to assist mathematical reasoning: Proceedings of a workshop, National Academies Press, 2023, DOI 10.17226/27241. [RSST96] Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas, A new proof of the four-colour theorem, Electron. Res. Announc. Amer. Math. Soc. 2 (1996), no. 1, 17–25, DOI 10.1090/S1079-6762-96-00003-0. MR1405965 [RPBN?23] Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi, Mathematical discoveries from program search with large language models, Nature 625 (December 2023), no. 7995, 468–475, DOI 10.1038/s41586-023-06924-6. [Tao23] Terence Tao, Formalizing the proof of PFR in Lean4 using Blueprint: a short tour, 2023. https://terrytao./2023/11/18 [TWL?24] Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong, Solving olympiad geometry without human demonstrations, Nature 625 (January 2024), no. 7995, 476–482, DOI 10.1038/s41586-023-06747-5. [Wag21] Adam Zsolt Wagner, Constructions in combinatorics via neural networks, Preprint, arXiv:2104.14516, 2021. [WLGSB23] Y. Wang, C.-Y. Lai, J. Gómez-Serrano, and T. Buckmaster, Asymptotic self-similar blow-up profile for three-dimensional axisymmetric Euler equations using neural networks, Phys. Rev. Lett. 130 (2023), no. 24, Paper No. 244002, 6, DOI 10.1103/physrevlett.130.244002. MR4608987 [YSG?23] Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar, LeanDojo: Theorem proving with retrieval-augmented language models, Preprint, arXiv:2306.15626, 2023. https://www./journals/notices/202501/noti3041/noti3041.html https://terrytao./mastodon-posts/ https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0 小樂(lè)數(shù)學(xué)科普：使用新的開(kāi)源跨學(xué)科數(shù)據(jù)集訓(xùn)練AI人工智能模型像科學(xué)家那樣思考 小樂(lè)數(shù)學(xué)科普：每人最高可獲100萬(wàn)美元資助的AI for Math Fund數(shù)學(xué)人工智能基金成立——陶哲軒等人擔(dān)任顧問(wèn) 小樂(lè)數(shù)學(xué)科普：AI人工智能如何改變預(yù)測(cè)科學(xué)？——譯自Quanta Magazine量子雜志 小樂(lè)數(shù)學(xué)科普：獎(jiǎng)金$1048576=22?美金的人工智能奧數(shù)AI-MO進(jìn)步獎(jiǎng)開(kāi)賽2024-4-1~6-27 小樂(lè)數(shù)學(xué)科普：新的AI人工智能將如何影響數(shù)學(xué)研究？——Keith Devlin專(zhuān)欄《Devlin之角》 小樂(lè)數(shù)學(xué)科普：谷歌AI做題家AlphaGeometry解決幾何奧數(shù)題暫時(shí)拔得頭籌，登上Nature，但離$1000萬(wàn)獎(jiǎng)金仍有距離 小樂(lè)數(shù)學(xué)科普：1000萬(wàn)美元AI-MO獎(jiǎng)（人工智能奧數(shù)獎(jiǎng)）難度不亞于解決黎曼猜想？ 小樂(lè)數(shù)學(xué)科普：國(guó)產(chǎn)AI進(jìn)行時(shí)——用人工智能解數(shù)學(xué)題——好未來(lái)MathGPT測(cè)評(píng)
2024年度計(jì)算機(jī)科學(xué)進(jìn)展回顧——譯自量子雜志Quanta Magazine 數(shù)學(xué)界“諾獎(jiǎng)”菲爾茲獎(jiǎng)得主：學(xué)好數(shù)學(xué)有偏方 當(dāng)1+1+1等于1時(shí)——James Propp教授專(zhuān)欄 2025年AMS Steele斯蒂爾終身成就獎(jiǎng)授予Dusa McDuff杜薩·麥克達(dá)芙（含迄今全部歷史獲獎(jiǎng)人名單一覽） 2024年度數(shù)學(xué)進(jìn)展回顧——譯自量子雜志Quanta Magazine 數(shù)學(xué)就是不同的思維——《量子雜志》每周數(shù)學(xué)隨筆 【第3波】10本zzllrr小樂(lè)推薦精讀的國(guó)內(nèi)外優(yōu)秀數(shù)學(xué)科普書(shū)籍【平價(jià)優(yōu)選】【推薦日期2024-12-17】 璀璨成就的背后，19世紀(jì)的數(shù)學(xué)家一個(gè)比一個(gè)慘？ 《小樂(lè)數(shù)學(xué)科普》歷史文章合集2024-12-15 2025年AMS Steele斯蒂爾數(shù)學(xué)闡述獎(jiǎng)授予詹姆斯·S·米爾恩（James S. Milne）（含迄今全部歷史獲獎(jiǎng)人名單一覽） 使用新的開(kāi)源跨學(xué)科數(shù)據(jù)集訓(xùn)練AI人工智能模型像科學(xué)家那樣思考 每人最高可獲100萬(wàn)美元資助的AI for Math Fund數(shù)學(xué)人工智能基金成立——陶哲軒等人擔(dān)任顧問(wèn) 艾倫·海切爾（Allen Hatcher）榮獲首屆（2025）AMS斯坦因變革性闡述獎(jiǎng) 2024年我在計(jì)算機(jī)科學(xué)方面學(xué)到了什么——《量子雜志》每周數(shù)學(xué)隨筆 采訪(fǎng)數(shù)學(xué)家讓-皮埃爾·布吉尼翁Jean-Pierre Bourguignon（上）——譯自EMS歐洲數(shù)學(xué)會(huì)雜志 采訪(fǎng)數(shù)學(xué)家讓-皮埃爾·布吉尼翁Jean-Pierre Bourguignon（中）——譯自EMS歐洲數(shù)學(xué)會(huì)雜志 采訪(fǎng)數(shù)學(xué)家讓-皮埃爾·布吉尼翁Jean-Pierre Bourguignon（下）——譯自EMS歐洲數(shù)學(xué)會(huì)雜志 首屆（2025）AMS馬丁·艾薩克斯獎(jiǎng)授予英國(guó)數(shù)學(xué)家本·格林Ben Green 數(shù)學(xué)思維不是你想象的那樣——譯自量子雜志Quanta Magazine 數(shù)學(xué)史有什么用？——譯自Ben Orlin本·奧爾林的《數(shù)學(xué)和爛插畫(huà)》博客 【第2波】10本zzllrr小樂(lè)推薦精讀的國(guó)內(nèi)外優(yōu)秀數(shù)學(xué)科普書(shū)籍【平價(jià)優(yōu)選】【推薦日期2024-11-22】 Soheyla Feyzbakhsh因代數(shù)幾何的進(jìn)展榮獲大獎(jiǎng)——譯自倫敦帝國(guó)理工學(xué)院網(wǎng)站 數(shù)學(xué)大統(tǒng)一理論——《量子雜志》每周數(shù)學(xué)隨筆 解決問(wèn)題的熱情——印度女?dāng)?shù)學(xué)家Neena Gupta（妮娜·古普塔） 數(shù)學(xué)能拯救你的靈魂嗎？——James Propp教授專(zhuān)欄 2024年阿貝爾獎(jiǎng)得主訪(fǎng)談（下）：米歇爾·塔拉格蘭 Michel Talagrand——譯自EMS歐洲數(shù)學(xué)會(huì)雜志 2024年阿貝爾獎(jiǎng)得主訪(fǎng)談（上）：米歇爾·塔拉格蘭 Michel Talagrand——譯自EMS歐洲數(shù)學(xué)會(huì)雜志 2024年阿貝爾獎(jiǎng)授予Michel Talagrand米歇爾?塔拉格蘭，因在概率論和泛函分析方面的開(kāi)創(chuàng)性貢獻(xiàn)及應(yīng)用 阿貝爾獎(jiǎng)得主拉茲洛·洛瓦茲談?wù)撾x散數(shù)學(xué)和連續(xù)數(shù)學(xué)之間的模糊界限——譯自HLF海德堡桂冠論壇 【第1波】10本zzllrr小樂(lè)推薦精讀的國(guó)內(nèi)外優(yōu)秀數(shù)學(xué)科普書(shū)籍【平價(jià)優(yōu)選】【推薦日期2024-11-14】 AI人工智能如何改變預(yù)測(cè)科學(xué)？——譯自Quanta Magazine量子雜志 菲爾茲獎(jiǎng)得主吳寶珠談?wù)撡ち_瓦的不朽遺產(chǎn)——譯自HLF海德堡桂冠論壇 2024年Salem塞勒姆獎(jiǎng)授予Miguel Walsh（米格爾·沃爾什）和王藝霖（含迄今全部歷史獲獎(jiǎng)人名單一覽） 丹尼斯·沙利文對(duì)納維-斯托克斯方程的新解讀——譯自HLF海德堡桂冠論壇博客 2025年AMS Satter美國(guó)數(shù)學(xué)會(huì)薩特獎(jiǎng)授予Ana Caraiani（安娜·卡拉亞尼）（含迄今全部歷史獲獎(jiǎng)人名單一覽） GIMPS最新發(fā)現(xiàn)已知最大素?cái)?shù)——2 13?2????1 - 1（第52個(gè)梅森素?cái)?shù)M136279841） 一個(gè)世紀(jì)以來(lái)，看似簡(jiǎn)單的數(shù)學(xué)問(wèn)題取得了重大進(jìn)展——譯自量子雜志Quanta Magazine 數(shù)學(xué)紋身墨水方程——譯自HLF海德堡桂冠論壇博客 世界各地的四個(gè)數(shù)學(xué)博物館：從最古老到最新——譯自美國(guó)數(shù)學(xué)會(huì)通訊 陶哲軒——在泛代數(shù)領(lǐng)域的一個(gè)試點(diǎn)項(xiàng)目，旨在探索新的合作方式和使用機(jī)器輔助的方法？ 為什么我們需要數(shù)學(xué)家來(lái)理解時(shí)空——《量子雜志》每周數(shù)學(xué)隨筆 數(shù)學(xué)家發(fā)現(xiàn)新形狀用以解決數(shù)十年之久的幾何問(wèn)題——譯自Quanta Magazine Tony Phillips教授的數(shù)學(xué)讀報(bào)評(píng)論2024-06 關(guān)于形狀的兩種數(shù)學(xué)視角——《量子雜志》每周數(shù)學(xué)隨筆 2024科學(xué)探索獎(jiǎng)數(shù)學(xué)獎(jiǎng)授予兩位數(shù)學(xué)家單芃、姚方 素?cái)?shù)如何揭示數(shù)學(xué)的隱藏結(jié)構(gòu)——《量子雜志》每周數(shù)學(xué)隨筆 2024未來(lái)科學(xué)大獎(jiǎng)數(shù)學(xué)獎(jiǎng)授予孫斌勇教授 歡迎進(jìn)入折紙世界——譯自美國(guó)數(shù)學(xué)會(huì)AMS專(zhuān)欄 什么是束sheaf（層）？——譯自量子雜志Quanta Magazine 2024年ECM歐洲數(shù)學(xué)大會(huì)（第9屆）EMS歐洲數(shù)學(xué)會(huì)獎(jiǎng)得主名單揭曉（含迄今全部歷史獲獎(jiǎng)人名單一覽） 2024年ECM歐洲數(shù)學(xué)大會(huì)（第9屆）Lanczos蘭佐斯數(shù)學(xué)軟件獎(jiǎng)名單揭曉（含迄今全部歷史獲獎(jiǎng)人名單一覽） 2024年ECM歐洲數(shù)學(xué)大會(huì)（第9屆）Paul Lévy保羅·萊維概率論獎(jiǎng)名單揭曉（含迄今全部歷史獲獎(jiǎng)人名單一覽） 2024年國(guó)際數(shù)學(xué)物理大會(huì)ICMP亨利·龐加萊獎(jiǎng)（Henri Poincaré Prize）名單揭曉（含迄今全部歷史獲獎(jiǎng)人名單一覽） 2024年第二屆ICBS國(guó)際基礎(chǔ)科學(xué)大會(huì)學(xué)術(shù)報(bào)告演講者及演講主題摘要（2024年7月15日周一） 2024年Wolf沃爾夫獎(jiǎng)數(shù)學(xué)獎(jiǎng)得主出爐：諾加·阿?。∟oga Alon）、阿迪·薩莫爾（Adi Shamir） 為什么這種形狀堆積起來(lái)如此之差？——譯自量子雜志Quanta Magazine 裁決中的P與NP以及復(fù)雜性的復(fù)雜度——譯自HLF海德堡桂冠論壇博客 龐加萊之家Maison Poincaré——法國(guó)數(shù)學(xué)博物館——譯自EMS歐洲數(shù)學(xué)會(huì)雜志 大腦如何思考數(shù)字——《量子雜志》每周數(shù)學(xué)隨筆 對(duì)話(huà)德國(guó)數(shù)學(xué)家馬丁·格羅切爾Martin Gr?tschel——數(shù)據(jù)驅(qū)動(dòng)數(shù)學(xué)的未來(lái) 2的平方根如何成為一個(gè)數(shù)字——譯自量子雜志Quanta Magazine 數(shù)學(xué)“在我的廚房里”——2024歐洲數(shù)學(xué)會(huì)EMS西蒙·諾頓數(shù)學(xué)推廣獎(jiǎng)授予Nina Gasking（尼娜·加斯金） 隨機(jī)性所具有的反直覺(jué)力量——《量子雜志》每周數(shù)學(xué)隨筆 在高度連通的網(wǎng)絡(luò)中，必有一個(gè)環(huán)路——譯自量子雜志Quanta Magazine · 開(kāi)放 · 友好 · 多元 · 普適 · 守拙 · 讓數(shù)學(xué) 更加 易學(xué)易練 易教易研 易賞易玩 易見(jiàn)易得 易傳易及 歡迎評(píng)論、點(diǎn)贊、在看、在聽(tīng) 收藏、分享、轉(zhuǎn)載、投稿 |
|
|
來(lái)自： zzllrr小樂(lè) > 《待分類(lèi)》
