陶哲軒：計算機輔助數學證明的歷史_風聞

導讀

幾個世紀以來，計算機（機器）一直是數學家的好朋友，他們利用它計算、提出猜想以及進行數學證明。隨着交互式定理證明器、機器學習算法和生成式AI等更為先進的工具的出現，機器被更具創新性和深度的方式得到運用。

近日，在MSRI（美國數學科學研究所，現改名SLMath）四十週年慶典上，陶哲軒（Terence Tao）對機器輔助數學證明的歷史和最新發展進行概述，並對數學中的機器輔助將扮演的未來角色進行預測。

他表示：早期的計算機輔助的數學研究以女性為主，並衍生出了一個計算能力單位：“千女時”，一千個使用加法器的女性能完成多少計算。“千女時”的出現也標誌着大規模計算的起源。

而現在的計算機已經超越了“暴力窮舉”，它逐漸能夠提供創造性的建議，幫助人們在數學研究中找到新的方向和靈感。尤其是GPT-4：“與這些先進的語言模型進行對話，能以間接的方式激發其數學思維，它就像一個非常耐心的同事，善於傾聽而不評判。”

對於未來計算機在數學中作用，陶哲軒説道：“人類與計算機在數學創造領域的貢獻比是95%和5%，那麼再過十年或者二十年，這個比例就會變成五五開”。

推薦理由：希望以此為契機，呼籲研究者關注AI在輔助數學證明方面發揮的驚人作用，機器學習提供了強大的框架，為數學家開闢了新思路。未來，AI有巨大的潛能幫助解決那些對人類來説極具挑戰性的數學難題，模擬和執行高級數學運算，乃至提出新的數學猜想和理論。以下為演講全文，編輯做了不改變原意的編譯，請欣賞：

視頻地址：https://vimeo.com/817520060

曾有人詢問我美國數學科學研究所（MSRI）以及數學的發展方向時，我認為計算機在數學領域的應用和作用將會變得越來越重要。

計算機已經在數學交流中發揮出重要的作用，例如用LaTeX進行寫作，用電子郵件、視頻會議與合作者進行溝通。在純數學方面，計算機的作用還沒受到重視，但情況正在改變。

過去，人類與計算機在數學創造領域的貢獻比是95%和5%，那麼再過十年或者二十年，這個比例就會變成五五開。要達到5（人）:95（計算機），可能還需要花費很長的時間。

早期的機器與數學：人工的、機械的，女性主導的

早期計算機的關鍵詞是人工、機械，在18和19世紀，計算機的主要作用是進行數字計算、建立對數表和三角函數表。

在20世紀20年代，物理學家亨德里克·洛倫茲利用人工計算機團隊來模擬大壩（阿夫斯呂伊特戴克）周圍的水流。這是一個重要的工程項目，需要進行大量複雜的計算，洛倫茲和他的團隊採用了浮點運算，這是一種在當時並不常見的計算方法。

在戰爭前計算機已經可以部分求解偏微分方程了。在第一次世界大戰和第二次世界大戰中，計算機幫助人類在彈道學、導航、曼哈頓計劃等方面進行了大量的數學計算。實際上，大部分工作是由人工計算機完成的，這些人工計算機主要由女性操作。因為當時的男性正在參戰。這也衍生出了一個計算能力單位：“千女時”，一千個使用加法器的女性能完成多少計算。“千女時”的出現也標誌着大規模計算的起源。

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

研究型數學家是如何使用計算機的呢？除了建立表格等之外，最早的用途之一就是做出猜想。18世紀高斯和勒讓德（Gauss and Legendre）在研究素數時利用大規模人工計算機構建了大量素數的表格，用於“猜想”素數分佈的規律。

圖注：勒讓德的素數分佈猜想公式

儘管勒讓德的素數分佈猜想在精確性上存在一些問題，但它的影響力仍然非常大。後來，這個猜想被狄利克雷修正為一個更準確的形式，這個形式現在已經被廣泛接受並被納入教科書。

圖注：狄利克雷修正後的公式

計算機加持下的數值計算現在已經成為解析數論中的常規工具，被用來幫助形成和驗證猜想。伯奇和斯温內頓-戴爾猜想就是一個很好的例子，這個未解的數學問題是通過大量的數值計算和數據分析來提出的。

圖注：能量均分定理表達式

電子計算機時代：點開多項數學輔助技能樹

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

圖注：實驗結果表示能量並不均分，找到的是穩定局部解（孤波）

但實際運行數值模擬時，結果並未符合他們預期的能量均分定理。起初，他們設定了一個初始狀態，其中只有一個粒子的能量被激發。然而，隨着時間的推移，能量並沒有均勻分佈，而是出現了在某一兩個粒子之間的長期穩定。也就是就是出現了孤波（或叫孤子）的現象。

然而，用計算機進行長時間運行實驗，現象會消失，能量最終會均勻分佈。

這種現象的出現是因為他們研究的系統其實是一個完全可積系統——投達晶格方程（Toda lattice equations）亦稱投達鏈——的近似。在這個完全可積系統中，孤子是會永久存在的。而他們實際的系統並不是完全可積的，但卻足夠接近，以至於他們能在模擬實驗中看到孤子現象。

這個具有巨大影響力的數值實驗開啓了可積系統的研究，也開啓了孤波的穩定性研究，這個研究領域至今仍然活躍。

圖注：阿佩爾和沃夫岡·哈肯在1976年用計算機輔助證明了四色定理。

在現代電子計算機的初期，計算機的威力在於它們能夠揭示出一些“意料”之外的現象。四色定理可能是大家最熟知的一個通過計算機得證的定理。在其證明中，凱尼斯·阿佩爾（Kenneth Appel）和沃夫岡·哈肯（Wolfgang Haken）編寫了一些特定的程序，這些程序可以處理特定的圖，並通過計算機檢查這些圖的某些性質。如果某一特定的圖能夠滿足這些性質，那麼就能用四種顏色來對其進行着色。這就是通過計算機得以證明的四色定理。

四色定理的證明分為兩個主要部分：可歸化和不可避免性。可歸化部分表明，任何包含1834種配置中的任何一種的圖都可以轉換為更小的圖，且如果更小的圖可以四色着色，那麼原圖也可以。這部分證明是通過將這些配置逐個輸入計算機完成的。

不可避免性部分表明，如果存在一個不能四色着色的圖，那麼它必須包含1834種配置中的至少一種，這部分通過手動檢查超過400頁的微縮膠片來驗證。

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

開普勒猜想是另一個計算機輔助數學證明的例子。在17世紀，開普勒研究了三維空間中單位球體的最密集堆積方式，發現兩種堆積方式，即六方緊密堆積和立方緊密堆積，它們的密度都約為74%。開普勒猜測這是堆積密度的最大可能值，沒有其他堆積方式可以超過這個密度。這個猜想至今仍是一個重要的數學問題。

開普勒猜想本質上是一個涉及無窮多變量的優化問題，這使得它並不容易通過計算機驗證。儘管在1951年，Toth提出了一種可能的解決方法，即通過有限多個沃羅諾伊單元的體積上的某些加權不等式來尋找球體堆積密度的上界，但是，儘管經過多次嘗試，但並沒有找到能得出精確結果的有説服力的證明。

托馬斯·海爾斯（Thomas Hales）和塞繆爾·弗格森（Samuel Ferguson）採取了一種靈活求解最小化問題的策略：調整評分函數，但這反過來又會產生更多的問題。然而，儘管評分函數變得越來越複雜，但他們的任務在某種程度上卻變簡單了。數篇論文發表後，兩位學者終在1998年成功證明了開普勒猜想，證明方式是用線性規劃設計出了一個複雜的評分函數。

據説，海爾斯最初並不打算使用計算機來幫助他證明這個猜想，但隨着項目變得越來越複雜，他發現他必須要依賴計算機。最後他們的證明包含了250頁的數學筆記，以及3GB的計算機代碼、數據和結果。

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

近年來，彼得·舒爾茨（Peter Scholze）的液態張量實驗無疑是最為人所知的形式化證明實驗項目，涉及舒爾茨的"凝聚態數學"理論（condensed mathematics），目標是修復拓撲空間類別的一些問題，如拓撲阿貝爾羣，方式是使用“凝聚”的新的數學對象來替代傳統的拓撲空間類別。

“凝聚數學”理論中的一個關鍵結果是“消失定理”， 研究發現，在特定的數學結構中，某些元素或屬性在一定條件下會“消失”。消失定理是凝聚數學中的核心，它是使用凝聚數學進行泛函分析研究的基礎。證明這個定理非常困難，舒爾茨花了一年研究，但進展緩慢。

於是，舒爾茨發起“液態張量實驗”，希望用數學軟件Lean對結果進行形式化，實現過程中，他們將幾個基礎的數學理論添加到了Lean的mathlib庫中。最後，在舒爾茨和其團隊的努力下，2021年5月，形式化了一個關鍵的子定理，2022年7月得到了完整定理的形式化。該項目的主要成就在於大幅擴充了Lean的數學庫。事實上，由於該項目構建的豐富庫例程，其他的Lean形式化項目變得更加便捷和高效。