圖源：Terence Tao|AMS Notice

作者：陶哲軒（加州大學洛杉磯分校數學教授）AMS Notice 202501

譯者：zzllrr小樂（數學科普公眾號）2024-12-25

幾個世紀以來，數學家一直依靠計算機（人類、機械或電子）和機器來協助他們的研究（如果考慮到算盤等早期計算工具，甚至幾千年）。例如，自從納皮爾（John Napier，1550 - 1617）等人的早期對數表以來，數學家就知道構建數學對象的大型數據集來執行計算和做出猜想的價值。勒讓德（Adrien-Marie Legendre，1752 - 1833）和高斯（Carl Friedrich Gauss，1777 - 1855）使用人類計算機編制的大素數表來猜想現在所謂的素數定理（PNT）；一個半世紀后，伯奇（Bryan John Birch，1931 -）和斯溫納頓-戴爾（Peter Swinnerton-Dyer，1927 - 2018）同樣使用早期電子計算機生成有限域上橢圓曲線的足夠數據，以提出他們自己對這些對象的著名猜想（即BSD猜想）。毫無疑問，許多讀者已經利用了最廣泛的數學數據集之一——整數數列在線百科全書（OEIS），它產生了無數猜想以及在不同數學領域之間意想不到的聯系，并為研究人員提供了一個有價值的數學對象的文獻搜索引擎。他們不知道該數學對象的名稱，但可以將其與整數序列相關聯。在21世紀，此類大型數據庫還可以作為機器學習算法的關鍵訓練數據，這些算法有望實現自動化或者至少大大簡化數學猜想和聯系的生成過程。

除了數據生成之外，計算機的另一個重要用途是科學計算，如今科學計算被大量用于數值求解微分方程和動力系統，或計算大型矩陣或線性算子的統計數據。這種計算的早期例子出現在1920年代，當時亨德里克·洛倫茲（Hendrik Lorentz，1853 - 1928）組建了一組人類計算機來模擬阿夫魯戴克大壩（Afsluitdijk，當時荷蘭正在建設的一座水壩）周圍的流體流動；除其他外，該計算因開創了現在標準的浮點運算裝置而聞名。但現代計算機代數系統（CAS，例如Magma、SAGEMath、Mathematica、Maple等）以及更通用的編程語言可以遠遠超出傳統的“數字運算”；它們現在通常用于執行代數、分析、幾何、數論和許多其他數學分支中的符號計算。由于舍入誤差和不穩定性，某些形式的科學計算是眾所周知的不可靠，但人們通?？梢杂酶鼑栏竦姆椒▉泶孢@些方法（例如，用區間算術代替浮點算術），這可能會增加運行時間或內存使用量。

計算機代數系統的近親是可滿足性（SAT，satisfiability）求解器和可滿足性模理論 (SMT，satisfiability modulo theory) 求解器，它們可以根據某些受限制的假設集合對結論進行復雜的邏輯推導，并為每個此類推導生成證明證書。當然，可滿足性是一個 NP完全問題，因此這些求解器的規模不會超過某個臨界點。以下是使用SAT求解器證明結果的典型示例：

定理 0.1 （布爾勾股數三元組定理【HKM16】）

集合{1, ? ,7824}的元素可以分為兩類，使得每一類中都不包含勾股數三元組——滿足a2+b2=c2的(a,b,c)；然而，對于集合{1, ? ,7825}這是不可能的。

該證明需要4個CPU年的計算并生成200TB的命題證明，后來被壓縮到68GB。

當然，數學家也經常使用計算機來完成日常任務，例如撰寫論文以及與合作者交流。但近幾十年來，出現了幾種利用計算機輔助數學研究的有前途的新方法：

• 機器學習算法可用于發現新的數學關系，或生成數學問題的潛在示例或反例。

• 形式證明助手可用于驗證證明（以及大語言模型的輸出），允許真正大規模的數學協作，并幫助構建數據集來訓練上述機器學習算法。

• ChatGPT等大語言模型（有可能）被用來使其他工具更容易、更快速地使用；它們還可以建議證明策略或相關工作，甚至直接生成（簡單的）證明。

這些類型的工具中的每一種都已經在不同的數學領域找到了合適的應用，但我發現特別有趣的是將這些工具組合在一起的可能性，用一種工具抵消另一種工具的弱點。例如，形式證明助手和計算機代數包可以過濾掉現在臭名昭著的大語言模型看似合理的廢話的“幻覺”傾向，而反之，這些模型可以幫助自動化證明形式化中更繁瑣的方面，并提供用于運行復雜符號或機器學習算法的自然語言界面。其中許多組合仍僅處于概念驗證開發階段，該技術需要一定的時間才能變得成熟起來成為數學家真正有用且可靠的工具。然而，早期的實驗似乎確實令人鼓舞，我們應該期待在不久的將來會出現一些令人驚訝的新數學研究模式的演示；它不是科幻小說中可以自主解決復雜數學問題的超級智能人工智能，而是一個有價值的助手，可以提出新想法、過濾錯誤、執行例行案例檢查、數值實驗和文獻評審任務，讓人類數學家能夠在項目中注重對高層概念的探索。

1. 證明助手

當然，計算是使用計算機執行的這一事實并不能自動保證其正確。計算可能會產生數值誤差，例如由于用離散近似值替換連續變量或方程而引起的誤差。代碼中可能會無意中引入錯誤，或者輸入數據本身可能包含不準確之處。即使計算機用來運行代碼的編譯器也可能存在缺陷。最后，即使代碼完美執行，代碼正確計算的表達式也可能不是數學論證真正想要的表達式。

早期的計算機輔助證明遇到了許多這樣的問題。例如，凱尼斯·阿佩爾（Kenneth Appel，1932 - 2013）和沃夫岡·哈肯（Wolfgang Haken，1928 - 2022）在1976年對四色定理【AH89】的原始證明圍繞著一系列1834個需要遵守兩個性質稱為“可歸約性”（reducibility）和“不可避免性”（unavoidability）的圖?？梢酝ㄟ^每次將每個圖輸入一個定制的軟件來檢查可歸約性；但不可避免的是，需要進行繁瑣的計算，包括數百頁的縮微膠片——通過哈肯的女兒Dorothea Blostein（多蘿西婭·布洛斯坦）的英勇努力手工驗證——最終包含多個（可修復的）錯誤。1994年，Robertson、Sanders、Seymour和 Thomas【RSST96】試圖使Appel–Haken證明的計算部分完全可由計算機驗證，但最終卻產生了一個更簡單的論證（僅涉及633個圖，以及驗證不可避免性的更簡單的程序），可以通過用任意數量的標準編程語言編寫的計算機代碼更有效地驗證。

證明助手將這種形式化更進一步，作為一種特殊類型的計算機語言，其設計目的不是執行純粹的計算任務，而是驗證邏輯或數學論證結論的正確性。粗略地說，數學證明中的每個步驟都對應于該語言中的多行代碼，并且只有在證明有效的情況下才能編譯整個代碼?，F代證明助手，例如Coq、Isabelle或Lean，有意嘗試模仿數學寫作的語言和結構，盡管它們在許多方面通常更加挑剔。舉一個簡單的例子，為了解釋一個數學表達式，例如a?,形式的證明助手可能需要精確指定基礎變量a,b的“類型”（例如，自然數、實數、復數），以便確定正在使用哪種求冪運算（這對于諸如0?的表達式尤其重要，在不同的求冪概念下，其解釋略有不同）。人們投入了大量精力來開發自動化工具和廣泛的數學結果庫來管理形式證明的這些低級方面，但在實踐中，數學論證的“明顯”部分通常比“重要”部分需要更長的時間才能形式化。舉一個例子：給定三個集合A?,A?,A?，數學家可能會相互切換使用笛卡爾積(A?×A?)×A?, A?×(A?×A?)和∏_{i∈{1,2,3}}A?，因為它們“顯然”是“同一”對象；但在大多數數學形式化中，這些乘積實際上并不相同，并且論證的形式化版本可能需要投入一部分證明來在這些空間之間建立適當的等價性，并確保涉及該乘積的一個版本的陳述對于另一個版本繼續成立。

由于這個和其它的原因，將人類數學家（即使是非常仔細的數學家）編寫的證明轉換為在形式證明助手中編譯的形式證明的任務相當耗時，盡管隨著時間的推移，這個過程逐漸變得更加高效。上述四色定理由Werner和Gonthier于2005年【Gon08】在Coq中形式化。關于3中對單位球最密堆積的臭名昭著的開普勒猜想的證明由Hales和Ferguson在1998年【Hal05】的一個非常復雜的（計算機輔助的）證明中證明。2003年，Hales啟動了Flyspeck項目來形式化地驗證證明，預計需要20年才能完成，盡管最終通過Hales和其他21位貢獻者的合作，“僅”用了11年就實現了這一目標【HAB?17】。最近，舒爾茨（Peter Scholze，1987 -）于2019年啟動了“液體張量實驗” 【Com22】，形式驗證了他和克勞森（Dustin Clausen）關于凝聚態數學理論中“液體向量空間”的某個Ext群消失的基本定理。人類寫的證明“只有”十頁長，盡管包含大量凝聚態數學的先決材料；盡管如此，通過大量的協作努力，Lean的形式化花費了大約18個月的時間。我本人領導了一項關于高爾斯、格林、曼納斯和我自己的加性組合猜想【GGMT23】最近證明的形式化工作【Tao23】；人工編寫的證明長達33頁，但基本上是自給自足的，大約20名合作者組成的小組在三周內將其形式化。有些數學領域比其他領域更難以形式化；凱文·巴扎德（Kevin Buzzard，1968 -）最近宣布了一項形式化費馬大定理證明的項目，他估計至少需要五年時間完成。

考慮到所需的所有努力，數學證明的形式化工作對數學的價值是什么？最明顯的是，它為給定結果的正確性提供了極高的置信度，這對于有爭議或因強烈吸引虛假證明而臭名昭著的結果特別有價值，或者對于審閱人愿意逐行驗證此類特別冗長的證明的領域尤其供不應求。（理論上，證明助手編譯器中仍然可能存在隱藏的缺陷 - 故意將其保持得盡可能小以減少這種可能性 - 或者結果的形式聲明中使用的定義可能在微妙但重要的方面與人類可讀的陳述有所不同，但這種情況不太可能發生，特別是如果形式證明密切跟蹤人類編寫的證明的前提下。）形式化過程通常會發現人類證明中的小問題，有時可以揭示論證的簡化或強化，例如通過揭示一個看似重要的假設在引理中實際上是不必要的，或者可以使用低功效但更通用的工具來代替高級但專門的工具。采用現代語言（例如Lean）的形式化項目通常會將項目過程中生成的許多基本數學結果貢獻到公共數學庫中，這使得未來形式化項目更容易進行。

但形式證明助手也可以實現數學教育和協作的新模式。幾個實驗項目正在進行中，以獲取形式證明并將其轉換為更易于人類理解的形式，例如一段交互式文本，其中論證中的各個步驟可以擴展為更詳細的內容或折疊為高級摘要；這可能是一種特別適合未來數學教科書的格式。傳統的數學合作很少涉及超過五個左右的共同作者，部分原因是每個共同作者都需要信任和驗證其他人的工作；但形式化項目通常會涉及數十名之前沒有互動過的人，這正是因為形式證明助手允許項目中的各個子任務獨立于其他子任務進行精確定義和驗證?？梢韵胂螅@些證明助手還可以允許類似的分工來生成新的數學結果，從而允許比以前的在線協作（例如“Polymath”項目【Gow10】，其規模由于需要對討論進行人工審核而受到限制）規模大得多的高度并行和眾包協作。隨著時間的推移，其他科學或軟件工程項目中已經建立的大型合作也可能在研究數學中變得司空見慣。一些貢獻者可能扮演“項目經理”的角色，例如專注于建立精確的“藍圖”，將項目分解為更小的部分，而其他貢獻者則可以專門研究項目的各個組成部分，而不必具備理解整個項目所需的所有專業知識。

然而，在此之前，形式化過程需要變得更加高效?！癲e Bruijn因子”（編寫正確的形式證明與正確的非形式證明的難度之間的比率）仍然遠高于1（我估計約為20)，但在下降中。我相信將該比率降至1以下不存在根本障礙，尤其是因為AI、SMT求解器和其他工具的集成度不斷提高；這將給我們的領域帶來變革。

2. 機器學習

機器學習是指訓練計算機執行復雜任務的一系列技術，例如預測與來自非常廣泛的類別的給定輸入相對應的輸出，或者辨別數據集中的相關性和其他關系。許多流行的機器學習模型使用某種形式的神經網絡來編碼計算機如何執行任務。這些網絡是由大量簡單運算（線性和非線性）組合在一起形成的許多變量的函數；通常，人們會為這樣的網絡分配某種獎勵函數（或損失函數），例如通過根據訓練數據集憑經驗測量其性能，然后執行計算密集型優化以找到該網絡的參數選擇使得獎勵函數盡可能大（或損失函數盡可能?。?。這些模型具有無數的實際應用，例如圖像和語音識別、推薦系統或欺詐檢測。然而，它們通常不能提供強有力的準確性保證，特別是當應用于與訓練數據集顯著不同的輸入時，或者當訓練數據集有噪聲或不完整時。此外，模型通常是不透明的，因為很難從模型中提取人類可以理解的解釋來說明模型為什么做出特定的預測，或者理解模型的一般行為。因此，這些工具乍一看似乎不適合研究數學，因為人們既希望得到嚴格的證明，又希望對論證有直觀的理解。

盡管如此，最近出現了一些有前景的用例，即適當選擇的機器學習工具可以產生或至少提出新的嚴格數學，特別是與其他可以驗證這些工具輸出的更可靠技術相結合時。例如，流體方程數學理論（例如歐拉方程或納維-斯托克斯N-S方程）的一個基本問題是能夠嚴格證明解u在有限時間內從光滑的初始數據開始有限時間內爆破。最臭名昭著的例子涉及三維不可壓縮納維-斯托克斯方程，該方程的解是（未解決的）千禧年獎問題之一；這仍然遙不可及，但最近在其他流體方程方面取得了進展，例如二維的Boussinesq方程（三維不可壓縮歐拉方程的簡化模型）。建立這種奇點（singularity）的一種途徑是構建自相似的爆破解u，由解出一個更簡單的偏微分方程（PDE）的低維函數U描述。該偏微分方程的封閉形式解似乎不可用；但如果能夠產生這個偏微分方程的足夠高質量的近似解?（近似服從某些邊界條件），可以通過應用微擾理論嚴格證明精確解U（例如基于不動點定理的理論）。傳統上，人們會使用數值PDE方法來嘗試產生這些近似解?，例如，通過將偏微分方程離散化為差分方程（difference equation），但使用此類方法獲得具有所需精度水平的解的計算成本可能很高。Wang、Lai、Gómez-Serrano和Buckmaster【WLGSB23】于2019年提出了另一種方法，他們使用經過訓練的物理信息神經網絡（PINN，Physics Informed Neural Network）來生成函數?，可以最小化一個合適的損失函數，該函數度量了近似遵守所需偏微分方程和邊界條件的程度。由于這些函數?通過神經網絡而不是方程的離散版本生成，它們可以更快地生成，并且可能不易受到數值不穩定的影響。事實證明，Chen和Hou的同期工作【CH22】能夠使用更傳統的數值方法為該方程建立有限時間爆破解；然而，機器學習范式顯示出作為此類偏微分方程問題的補充方法的巨大潛力。例如，我們可以設想一種混合方法，其中人類數學家首先提出一個爆破模擬，然后神經網絡嘗試找到一個粗略的近似解，然后使用更傳統的數值方法將該解細化得足夠準確，使得可以對其應用嚴格的穩定性分析。

機器學習在數學中應用的另一個例子是紐結理論（knot theory）領域。結具有極其多樣化的拓撲不變量：結的符號差（signature）是與以結為邊界的表面（Siefert曲面）的同調性相關的整數；結的Jones瓊斯多項式可以使用辮子（braid）的表示理論來描述；大多數結（不包括環面結torus knot）其補（complement）具有典范雙曲幾何，可用于描述許多雙曲不變量，例如雙曲體積等等。先驗地，這些來自不同數學領域的不變量之間的相互關系并不明顯。然而，2021年，Davies、Juhász、Lackenby和Tomasev【DJLT21】通過機器學習研究了這個問題。通過在現有的近200萬個結（加上100萬個隨機生成的額外的結）的數據庫上訓練神經網絡，他們能夠使該神經網絡模型從大約兩打雙曲不變量中高精度地預測結的符號差。然而，生成的預測函數非常不透明，并且最初并沒有揭示出關于符號差和雙曲不變量之間的精確關系的更多見解。然而，可以通過一種稱為顯著性分析（saliency analysis）的簡單工具進一步進行，粗略地說，該工具測量每個單獨的雙曲不變量對預測函數的影響。該分析表明，在使用的兩打雙曲不變量中，只有其中三個（縱向平移以及子午平移的實部和復數部分）對預測函數有顯著影響。通過視覺上檢查這三個不變量的符號差散點圖，作者能夠推測出這些數量之間更容易理解的關系。進一步的數值反駁了他們最初的猜想，但提出了他們能夠嚴格證明的猜想的修改版本。機器生成的猜想與人類使用理論進行驗證（和修改）之間的相互作用是一個有前途的范式，似乎適用于許多其他數學領域。

機器學習的許多應用需要大量的訓練數據，理想情況下以某種標準化格式（例如數字向量）表示，以便現有的機器學習算法可以相對輕松地應用于其中。數據的精確表示至關重要；機器學習算法可以很容易地在一種數據表示中發現數據不同組成部分之間的相關性，但在另一種數據表示中幾乎不可能找到。雖然數學的一些領域開始編制有用對象的大型數據庫（例如，結、圖或橢圓曲線），但仍然有許多重要類別的更模糊定義的數學概念尚未系統地放入可用于機器學習的形式中。例如，回到偏微分方程的例子，文獻中研究了數千種不同的偏微分方程，但通常在符號和項的代數排列方面具有很大的可變性，而且沒有什么類似于通常所研究的偏微分方程的標準數據庫（例如，研究它們是橢圓形、拋物線形還是雙曲形；解的存在性和唯一性、守恒定律等已知的信息）。這樣的數據庫可能有助于根據其他偏微分方程的結果對一個偏微分方程的行為進行推測性預測，或者建議從一種偏微分方程到另一種偏微分方程的可能類比或化簡；但由于缺乏任何規范范式來表示此類方程（或至少缺乏識別它們的“指紋” 【BT13】），因此目前構建這樣的數據庫都非常困難，更不用說將其輸入神經網絡了。可以想象，未來的證明形式化和人工智能的進步可能會使生成和利用此類數據庫（可能包含“真實世界”和“合成”數據集）變得更加可行。

3. 大語言模型

大語言模型（LLM）是一種相對較新的機器學習模型，適合對極其廣泛和大型的自然語言文本數據集進行訓練。一種流行的大語言模型是GPT（Generative Pre-trained Transformer生成式預訓練轉換器），顧名思義，它是圍繞Transformer模型（一種神經網絡變體，旨在預測字符串中的下一個單詞即“token詞元”，并保留對字符串早期單詞的一些長期“注意力”，以模擬句子的上下文）構建的。通過迭代該模型，人們可以對給定的文本提示（prompt）生成冗長的文本響應。當使用少量數據進行訓練時，此類模型的輸出并不令人印象深刻，例如，并不比嘗試在智能手機上迭代“自動完成”文本輸入功能復雜多少，但經過對極大且多樣化的數據集進行大量訓練后，這些模型的輸出可以令人驚訝地連貫，甚至具有創造性，并且可以生成乍一看很難與人類書寫區分開的文本，盡管仔細檢查后，輸出通常是無意義的，并且與任何基本事實沒有聯系，這種現象被認為是“幻覺”（hallucination）。

人們當然可以嘗試應用這種通用的LLM來嘗試直接解決數學問題。有時，結果可能相當令人印象深刻；例如布貝克（Bubeck）等人記錄了一個案例，其中強大的大語言模型GPT-4能夠提供2022年國際數學奧林匹克問題的完整且正確的證明，該問題并不在該模型的訓練數據集中。相反，該模型不太適合執行精確計算，甚至基本算術；在一個例子【BCE?23】中，當要求計算表達式7×4 + 8×8時，GPT-4立即給出了錯誤答案120，然后繼續通過分步過程來證明計算的合理性返回正確答案92。當被問及這一差異時，GPT-4只表示其最初的猜測是一個“拼寫錯誤”（typo）。這些問題可以通過使用GPT-4的“插件”得到一定程度的補償，其中GPT-4被訓練為向外部工具（例如Wolfram Alpha）發送特定類型的查詢（例如數學計算），而不是通過其內部模型猜測答案，盡管目前工具之間的集成還不是無縫的。類似地，最近的概念驗證【RPBN?23】已經表明，LLM可用于查找組合學和計算機科學中各種問題的示例，這些示例優于以前的人類生成的示例，方法是要求這些模型生成程序來創建此類示例，而不是嘗試直接構建示例，然后使用另一種語言執行該程序來可靠地驗證輸出的質量，然后將其發送回原始模型以提示其對猜測進行改進。最近在使用LLM來增強現有符號證明引擎以解決狹窄類別的數學問題（例如奧林匹克幾何問題【TWL?24】）方面也取得了進展.

在我自己的GPT-4實驗中（可以在 https://terrytao.wordpress.com/mastodon-posts/ 找到），我發現最高效的用例是生成各種語言的基本計算機代碼（Python、SAGE、LaTeX、Lean、正則表達式等），或者清理凌亂且無組織的數據集（例如，在起初提供GPT-4一些所需參考書目條目格式的示例后，讓它將互聯網上抓取的一堆參考文獻整理成連貫的LaTeX參考書目）。在這種情況下，它通常會在第一次嘗試時產生令人滿意或接近令人滿意的輸出，只需進行少量修改即可獲得我正在尋求的輸出類型。我在讓GPT-4為實際數學問題推薦相關文獻或技術方面也取得了一些有限的成功。在一個測試用例中，我問它如何計算獨立隨機變量之和的尾部概率的指數衰減率，以在不給它提供大偏差理論（large deviation theory）等關鍵詞前提下，評估它是否知道這方面的相關定理（Cramér定理）。事實證明，GPT-4并沒有準確定位這個定理，而是產生了一串數學廢話，但奇怪的是，它確實引用了對數矩生成函數（logarithmic moment generating function），這是Cramér定理陳述中的一個關鍵概念，即使它似乎并不確切地“知道”這個函數與問題的相關性。在另一個實驗中，我向GPT-4詢問如何證明我正在研究的組合恒等式的建議。它給出了一些我已經考慮過的建議（漸近分析、歸納、數值）以及一些通用建議（簡化表達式、尋找類似問題、理解問題），而且還提出了一種技術（生成函數）我只是忽略了這一點，最終很容易地解決了這個問題。另一方面，這樣的建議列表對于新手數學家來說可能沒什么用，因為他們沒有足夠的經驗來獨立評估每個建議的有用性。盡管如此，我看到這些工具在提取用戶對一個問題的潛在知識方面的作用，只需成為一個好的傾聽者并提出足夠用戶給出專業評估的合理相關的想法即可。

Github Copilot（副駕駛）是另一個GPT模型，已集成到多個流行的代碼編輯器中。它經過不同語言的大型代碼數據集的訓練，旨在利用上下文線索（例如代碼中其他地方要執行的任務的非形式描述）為部分編寫的代碼提供自動完成建議。我發現它對于編寫數學LaTeX以及在Lean中形式化非常有效；事實上，它在我寫作時建議了幾句話，從而幫助我寫了這篇文章，其中許多句子我在最終版本中保留著或進行了輕微編輯。雖然其建議的質量差異很大，但有時它可以表現出對文本意圖的模擬理解的不可思議的水平。例如，在編寫另一篇關于如何估計積分的闡述性LaTeX筆記時，我描述了如何將積分分解為三個部分，然后詳細說明了如何估計第一部分。然后Copilot立即建議如何通過類似的方法來估計第二部分，并以完全正確的方式改變變量。這些頻繁經歷使我在LaTeX和Lean的寫作中獲得了小幅但明顯的加速，我預計這些工具在未來會變得更加有用，因為可以根據個人寫作風格和喜好“微調”這些模型。

4. 這些工具可以組合使用嗎？

上面討論的各種技術都有非常不同的優點和缺點，而且就其目前的發展水平而言，沒有一種技術適合作為數學家的通用工具，能與LaTeX或arXiv等無處不在的平臺相媲美。然而，最近有一些有希望的實驗可以通過將兩種或多種單獨的技術結合在一起來創建更令人滿意的工具。例如，在生成證明時對抗LLM的幻覺性質的一種可行方法是要求模型以形式證明助手的語言格式化其輸出，并將助手生成的任何錯誤作為反饋發送回模型。這個組合系統似乎適合生成簡單命題的簡短證明【YSG?23】；由于此類任務通常是有效形式化證明的限制因素，因此這種范式可以大大加快這種形式化的速度，特別是如果這些模型在形式化證明（而不是一般文本）上進行微調，并與更傳統的自動化定理證明方法集成，例如SMT求解器的部署。

由于能夠接受自然語言輸入，LLM還可能是一個用戶友好的界面，允許沒有特定軟件專業知識的數學家使用高級工具。如前所述，我和許多其他人已經經常使用此類模型來生成各種語言的簡單代碼（包括符號代數包），或創建復雜的圖表和圖像；似乎可以合理地預期，在不久的將來，人們還可以通過此類模型進行通信，僅使用高級會話指令來設計和操作像機器學習模型這樣復雜的東西。更雄心勃勃的是，人們可能希望最終能夠通過用自然語言向人工智能解釋結果來生成完整的研究論文（初稿），并完成形式驗證，人工智能將嘗試形式化結果的每一步并在需要澄清時詢問作者。

當前形式的形式化證明驗證的人力密集性質意味著當前研究論文的很大一部分實時完全形式化是不可行的。然而，許多已經用于驗證研究論文中特定計算密集型部分的工具（例如數值積分或 PDE求解器、符號代數計算或使用SMT求解器建立的結果）似乎可以進行修改之后出具形式證明證書。此外，可以以這種方式形式化的計算類別可以從當前實踐中大大擴展。僅舉一個例子，在偏微分方程領域，通常會使用大量計算來估計涉及一個或多個未知函數（例如一個偏微分方程的解）的某些積分表達式，并使用各種函數空間范數中此類函數的界限（例如Sobolev索博列夫空間范數），以及標準不等式（例如，H?lder霍爾德不等式和Sobolev索博列夫不等式），以及各種恒等式，例如分部積分或積分符號下的微分。此類計算雖然是常規計算，但可能包含不同嚴重程度的拼寫錯誤（例如符號錯誤），并且仔細審閱可能會很乏味，因為計算本身除了驗證最終估計值是否成立之外幾乎沒有提供任何見解?？梢韵胂螅梢蚤_發工具來以自動或半自動的方式建立此類估計，并且當前此類估計的冗長且無啟發性的證明可以由形式證明證書的鏈接取代。更雄心勃勃的是，人們可能能夠要求未來的AI人工智能工具在給定一組初始假設和方法的情況下產生最佳估計，而無需首先進行一些紙筆計算來猜測估計值是什么。目前，可能估計的狀態空間太復雜，無法以這種方式自動探索；但我認為隨著技術的進步，這種自動化沒有理由無法實現。當這種情況成為現實時，目前尚不可行的大規模的數學探索就成為可能。繼續以偏微分方程為例，該領域的論文通常一次研究一兩個方程；但在未來，人們可能能夠同時研究數百個方程，也許只為一個方程給出完整的論證，然后讓人工智能工具將論證適應一大族的相關方程，在推廣的論點非常規時詢問作者是否有必要擴展。這種大規模數學探索的一些提示開始在數學的其他領域出現，例如圖論中猜想的自動探索【Wag21】。

目前尚不清楚這些實驗中哪一個最終將最成功地為典型的數學家帶來先進的計算機輔助。一些概念證明目前無法擴展，特別是那些依賴于計算極其密集（且通常是專有）的人工智能模型，或需要大量專家人工輸入和監督的證明。然而，我對探索可能性空間的各種努力感到鼓舞，并相信在不久的將來會有更多執行機器輔助數學的新方法的例子。

5. 進一步閱讀

機器輔助證明的主題相當廣泛，分布在數學、計算機科學甚至工程學的各個領域；雖然每個單獨的子領域都有大量的活動，但直到最近才努力建立一個更加統一的社區，將此處列出的所有主題匯集在一起。因此，目前很少有地方可以找到對這些快速發展的數學模式的全面調查。一個起點是2023年6月美國國家科學院“人工智能輔助數學推理”研討會的會議記錄【Kor23】（作者是該研討會的聯合組織者之一）；作為該研討會的成果之一，Talia Ringer領導了一項為數學資源編譯AI的工作，其結果可以在https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0 中找到。

例如，該文檔中有一個指向“自然數字游戲”的鏈接，這是一種開始熟悉Lean證明輔助語言的易于訪問和交互的方式。這里討論的許多例子也取自2023年2月的IPAM研討會“機器輔助證明”（作者也參與共同組織），該研討會的演講可以在網上找到。

感謝匿名審稿人的指正和建議。

參考資料

[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.wordpress.com/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.ams.org/journals/notices/202501/noti3041/noti3041.html

https://terrytao.wordpress.com/mastodon-posts/

https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0

科普薦書

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

數學科普不迷路！