陶哲軒：AI正改寫數學規則、顛覆數學研究傳統

當全球最年輕的國際數學奧林匹亞金牌得主陶哲軒，站在2024年IMO講台上說出「我們用AI三週就完成了過去需要數年的數學證明」時，台下數百位各國數學天才們驚呆了。

這位13歲就拿下IMO金牌、現任UCLA教授的數學界傳奇人物，在這場演講中首度完整揭露了一個震撼事實：人工智慧正在以前所未有的方式重塑數學研究。從羅馬時代的算盤，到二戰期間被稱為「kilgirl」的人工計算員，再到今天能解IMO題目的GPT-4，機器輔助數學已有千年歷史。但真正的革命，才剛剛開始。

陶哲軒在這場名為「AI與數學」的演講中透露，當今數學研究正面臨三大技術突破：機器學習能發現人類從未察覺的數學連結、大型語言模型已開始解答奧數難題、而形式證明助手更讓20個數學家能在短短三週內協作完成複雜定理的證明。這些工具不僅改變了數學家的工作方式，更可能催生出前所未有的大規模數學探索時代。

從羅馬算盤到kilgirl：人類如何讓機器做數學

「機器輔助數學有多久的歷史？答案是數千年。」陶哲軒在演講一開始就拋出這個令人意外的觀點。他展示了羅馬人使用的算盤照片，指出這就是最早的數學機器之一。

但真正讓全場震驚的，是他對二戰時期「人工計算員」的描述。在電子計算機出現之前，「計算機」(computer)本身就是一個職業——專門負責計算的人。二戰期間，由於男性都上戰場了，美國軍方雇用了大量女性作為人工計算員，負責彈道計算等複雜運算工作。

「當時計算能力的基本單位不是CPU，而是『kilgirl』——1000個女孩工作一小時能完成的計算量。」陶哲軒的這個說法引發現場一陣驚嘆。這些女性計算員使用加法機等簡單工具，在程式設計師的指導下進行大規模數值計算，實際上就是現代分散式計算的雛形。

更早在18世紀，數學家就開始系統性地使用「人工計算機」來建立各種數學表格。著名的Napier對數表、三角函數表等，都是透過大量人工計算建立起來的。陶哲軒說：「當我還是高中生時，課程中還在教如何使用這些表格，但現在已經被計算機和電腦完全取代了。」

這些表格的影響力遠超過單純的計算工具。許多重要的數學發現都源自於表格中發現的規律。質數定理就是一個經典例子——高斯和其他數學家透過計算前一百萬個質數的表格，發現了質數分布的規律，提出了這個重要猜想，儘管正式證明要等到一個世紀之後。

現代數學家仍然大量依賴「表格」，只是現在我們稱之為資料庫。線上整數數列大全(OEIS)就是最著名的例子。陶哲軒解釋：「很多時候，當你研究一個問題時會遇到某個數列，比如1, 1, 2, 3, 5, 8, 13——你立刻知道這是費氏數列。OEIS收錄了數十萬個這樣的數列。」

這個資料庫經常能幫助數學家發現不同問題之間的意外連結。「你計算出某個問題的前幾項數值，輸入OEIS搜尋，如果幸運的話，會發現有人從完全不同的角度已經研究過相同的數列。這種巧合往往暗示著兩個看似無關的數學領域之間存在深層聯繫，許多重要的研究都是這樣開始的。」

當電腦開始證明定理：三大難題如何被攻克

科學計算的興起標誌著機器輔助數學進入新階段。陶哲軒認為，第一個真正的科學計算專案可以追溯到1920年代的亨德里克勞侖茲（Hendrik Lorentz）。荷蘭政府委託這位物理學家計算建造大型海堤對水流的影響，他必須求解複雜的流體力學方程式。

「勞侖茲使用了一大群人工計算員來解決這個問題，甚至為此發明了浮點運算。他意識到，如果要讓很多人快速進行大量計算，就需要一種能處理不同數量級數字的表示法。」這個發明後來成為現代電腦科學的基礎。

隨著電子計算機的普及，科學計算能力大幅提升。理論上，許多IMO幾何題都可以透過科學計算解決——將幾何問題轉換成代數方程組，然後用Sage或Maple等軟體暴力求解。但陶哲軒指出：「問題是，一旦規模超過某個臨界點，複雜度會呈指數甚至雙指數增長，直到最近都還不太可能用標準代數軟體暴力破解這些問題。但現在有了AI輔助，情況可能有所改觀。」

SAT求解器(satisfiability solver)的發展為解決特定類型的數學問題開闢了新路徑。這些工具專門處理邏輯謎題——給定一千個真假陳述和它們之間的約束條件，判斷是否存在滿足所有條件的解。更進階的SMT求解器還能處理包含變數和數學運算的約束。

儘管這些求解器的時間複雜度同樣會指數增長，但它們已經能解決一些重要問題。陶哲軒舉了一個令人震撼的例子：畢達哥拉斯三元組著色問題。

「問題是這樣的：如果你把所有自然數染成紅色或藍色，是否無論怎麼染色，至少有一種顏色會包含一組畢達哥拉斯三元組——三個數字能構成直角三角形的三邊，比如3, 4, 5？」

這個問題直到最近才透過大規模SAT求解器計算得到解答。「現在我們知道，你只需要考慮前7824個自然數。無論如何將這7824個數字染成兩種顏色，其中一種顏色必定包含畢達哥拉斯三元組。但從第7825個數字開始，就存在一種染色方法使得兩種顏色都不包含畢達哥拉斯三元組。」

這個證明需要檢查2的7824次方種染色可能，絕對不可能靠人工完成。最終的證明耗時數年計算，產生了200TB的證明檔案，後來壓縮到86GB。陶哲軒說：「這可能是人類永遠無法不借助電腦就完成的證明。」

四色定理的證明歷程更清楚地展現了電腦輔助證明的演進。1976年首次證明時，一半工作由電腦完成，一半由人工完成，過程中充滿錯誤和修正。「其中一位作者的女兒必須花費數小時手工檢查數千個子圖的可約性，非常繁瑣。」

真正的突破來自1990年代的簡化版證明，只需要檢查約700個圖形，所有計算都能用現代電腦在幾分鐘內完成。但要達到完全形式化——從數學公理開始逐步推導每一個步驟——則等到2005年才實現，使用的是名為Coq的證明助手語言。

開普勒猜想的證明過程最能說明大型電腦輔助證明的複雜性。這個17世紀的猜想問的是：球體的最密堆積方式是什麼？直觀上，水果攤的三角堆積法應該是最優的，密度約74%，但證明這點出奇困難。

Thomas Hales和他的團隊花了近十年時間發展出一套複雜的方法。他們將問題轉化為線性規劃，定義了特殊的「評分函數」來衡量不同堆積方式的效率。但這個方法太過靈活，每當遇到技術困難，他們就會調整評分函數，然後必須重新檢驗所有之前的工作。

「Sam Ferguson意識到，每次在嘗試最小化泛函時遇到問題，他都可以改變評分方式重新嘗試。但這意味著所有已經檢查的東西都要重做。評分函數變得越來越複雜，儘管每次修改都能節省幾個月到幾年的工作，但這種不斷調整讓同行很不耐煩。每次我在會議上報告進展時，都在最小化不同的函數，更糟的是，新函數與早期論文輕微不相容，需要回去修補舊論文。」

1998年，他們終於宣布成功，但這個證明包含250頁筆記和3GB的電腦程式與資料。《數學年刊》組織了12位審稿人花費四年時間審查，最終只能說「99%確信證明正確，但無法驗證電腦計算的正確性」。期刊史無前例地發表了這篇論文，但附加了編輯聲明。

直到2014年，Hales領導的Flyspeck專案才完成了這個證明的完全形式化，耗時12年，動用21位協作者。陶哲軒總結：「我們現在對這個結果有了完全的信心，但過程相當痛苦。」

當數學變成程式碼：Lean語言如何重塑證明

形式化數學的真正突破來自工具和方法論的進步。陶哲軒用Peter Scholze的故事展現了現代形式化的必要性和可能性。

Scholze是菲爾茲獎得主，以創立「濃縮數學」這個革命性領域而聞名。這個理論有望將代數方法應用到傳統上難以處理的函數分析問題上。但整個理論的基礎依賴於一個極其技術性的消失定理。

Scholze在個人部落格中坦承：「我花了整整一年時間專注於這個定理的證明，幾乎為此發瘋。最終我們能夠寫出論證，但沒有人敢檢查細節，所以我仍有揮之不去的疑慮。這個定理是濃縮形式主義能否成功應用於函數分析的關鍵，具有最重要的基礎意義，所以99.9%的確定性是不夠的。」

面對這個困境，Scholze決定將這個定理在Lean語言中完全形式化。Lean是近年來發展最快的證明助手語言，配備了眾包建立的大型數學函式庫。「與其從數學公理開始推導所有東西——這會變得非常繁瑣——Lean的中央數學函式庫已經證明了許多中級結果，包括微積分、群論、拓撲學等本科數學課程的基本定理。這樣你就有了一個起點——大約是研究生水平的數學教育——儘管距離你需要達到的水平還有很大差距，但確實有幫助。」

為了形式化Scholze的定理，團隊必須大幅擴充Lean的數學函式庫，加入同調代數、層理論、範疇論等高階領域。僅僅18個月後，他們就成功完成了形式化。「證明基本上是正確的。發現了一些小的技術問題，但沒有重大錯誤。他們還找到了一些不錯的簡化方法。有些技術步驟太難形式化，所以他們被迫找到捷徑。」

這個專案的真正價值在於它產生的副產品。首先，Lean的數學函式庫得到大幅擴充，現在能處理比以前更廣泛的抽象代數。其次，開發了一系列支援工具，後續的形式化專案都開始使用，包括陶哲軒自己的工作。

最重要的創新是「藍圖」(blueprint)工具。「直接嘗試形式化一個50頁的巨大證明真的很痛苦。你必須在腦中保持整個證明的結構。」新的工作流程是先將大證明分解成數百個小步驟，每個步驟都可以獨立形式化，然後再組合起來。

藍圖不僅幫助形式化，也成為人類閱讀證明的最佳方式。「如果你真的想以人類的方式閱讀證明，藍圖可能是現在最好的選擇。」

更令人興奮的是反向轉換技術的發展。現在有工具能將Lean中的形式證明轉換回人類可讀的格式。陶哲軒展示了一個例子：「這些文字都是從形式證明自動生成的。它看起來像人類證明，使用相同的數學語言，但更加互動。你可以點擊任何位置，它會告訴你當前的假設、你要證明的目標、變數是什麼。如果某個步驟太簡潔，你可以展開它，了解它的來源，甚至可以一直追溯到公理。」

陶哲軒預測：「我認為這很棒。未來的教科書將以這種互動方式編寫。先形式化，然後你就能擁有比現在更加互動的教科書。」

受到Scholze專案的啟發，陶哲軒啟動了自己的形式化專案。2023年，他與包括現場觀眾中的Tim Gowers在內的多位數學家合作，證明了一個組合數學定理——關於Hamming立方體中具有小倍增性質的子集的大小限制。

這個33頁的證明在創紀錄的3週內完成了形式化，動用了約20位協作者，使用了從Scholze專案發展出來的所有藍圖工具。「這可能仍然是形式化實際研究論文的最快紀錄。」

形式化使得數學證明變得更加開放和協作。「這讓證明工作變得更加開放和協作。你可以得到所有這些漂亮的視覺化。」陶哲軒展示了專案的依賴圖：目標定理位於圖底部，依賴於幾個其他陳述，這些陳述又依賴於更基礎的陳述。不同顏色表示不同的完成狀態——綠色表示已經形式化證明，藍色表示準備好形式化但尚未完成，白色表示連陳述都還沒有形式化。

「這個專案的美妙之處在於，你可以讓很多人獨立地協作完成這個圖的不同部分。每個小氣泡對應某個陳述，你不需要理解整個證明就能專注於你的小部分。」

參與者來自各個不同領域。「這是一個組合數學問題，但貢獻者包括概率論研究者、甚至非數學家的電腦程式設計師，他們非常擅長解決這些小型謎題類型的任務。每個人都挑選一個他們認為自己能完成的氣泡，然後去做。三週內我們就完成了整個專案。這真的是一個令人興奮的專案。」

傳統數學合作很少超過五人，因為需要相互信任每個人的數學都是正確的。「但在這樣的專案中，Lean編譯器自動檢查——你無法上傳不能編譯的東西，會被拒絕。所以你可以與素未謀面的人協作。」

形式化還帶來了意外的效率提升。儘管形式化一個證明比手寫需要大約10倍的時間，但修改證明時情況會逆轉。「舉例來說，我們的定理中出現了數字12，後來我們將其改進為11，得到稍微更強的定理。通常情況下你必須重寫整個證明，或者可能剪貼複製將12改為11，但你必須檢查沒有出錯。但當我們形式化後得到改進時，只用了幾天就將定理改為11。我們在某處將12改為11，然後編譯器會抱怨五個不同的地方現在某個特定部分不工作了，我們就可以進行針對性修復。」

對於特定類型的數學工作，形式化方法實際上已經更快了。目前有許多大型證明形式化專案正在進行，最大的是Kevin Buzzard的專案——獲得大筆資助來在Lean中形式化費馬最後定理。「他說最重要的部分需要五年時間。他不聲稱五年內能做完整個事情，但有趣的部分實際上已經在進行中了。」

機器學習、語言模型、證明助手：AI如何成為數學家夥伴

現代AI在數學中的應用可以分為三個主要方向，每個都展現出獨特的能力和限制。

機器學習在發現數學連結方面展現出令人驚喜的能力。陶哲軒詳細介紹了一個結理論的突破案例。結理論研究三維空間中的閉合曲線——也就是「結」，基本問題是判斷兩個結何時等價（能否透過連續變形將一個變成另一個而不讓線條穿越自身）。

數學家傳統上使用各種「結不變量」來區分不同的結。這些不變量分為兩大類：組合不變量（如簽名，透過計算結的交叉點得出的整數）和幾何不變量（如雙曲體積，來自結的幾何結構的實數或複數）。長期以來，沒有人知道這兩類不變量之間是否存在聯繫。

研究者建立了包含數百萬個結的資料庫，訓練神經網路學習這些資料。「他們發現，訓練後的神經網路90%的時間能夠根據所有雙曲幾何不變量正確預測簽名。所以它創造了這個黑盒子，告訴你簽名某種程度上隱藏在這些幾何不變量中，但沒有告訴你如何——它是個黑盒子。」

接下來的分析步驟展現了AI與人類智慧結合的威力。透過「顯著性分析」——逐個調整輸入變數觀察對輸出的影響——研究者發現在約20個輸入中，只有3個真正重要：縱向平移、經向平移的實部和虛部。「其他17個幾乎無關緊要，這三個並不是他們預期的。比如他們期望體積很重要，但體積幾乎無關緊要。」

有了關鍵變數，研究者就能直接繪製簽名與這三個輸入的關係圖，「然後他們可以用眼球——而不是神經網路，用人類網路——來看出明顯的模式」。

基於這些模式，他們提出了一個猜想，結果是錯的。「但他們用神經網路證明了它是錯的。然後根據失敗的方式，他們能夠修正它，找到了猜想的修正版本，實際上確實解釋了這個現象。一旦找到正確的陳述，他們就能證明它。所以他們實際上有了為什麼簽名與這些特定統計量如此密切相關的理論解釋。」

這個案例完美說明了機器學習在數學中的正確角色：「它不會直接為你解決問題，但它給你所有這些真正有用的提示，告訴你聯繫在哪裡、在哪裡尋找，但你仍然需要人類來實際建立聯繫。」

大型語言模型代表了AI輔助數學的另一個前沿。GPT-4的數學能力既令人印象深刻又充滿矛盾。陶哲軒展示了一個著名例子：GPT-4成功解決了2022年IMO的一道簡化版題目，給出了完整正確的解答。

「但這是一個極度精選的例子。我認為在他們測試的數百道IMO水平問題中，成功率約為1%。所以這個特定問題他們能夠解決，而且他們必須以正確的方式格式化問題才能得到解答，但這仍然相當驚人。」

同一個模型在基礎算術上的表現卻令人啼笑皆非。面對7×4+8×8這樣的簡單計算，GPT-4首先猜測答案是120，然後嘗試解釋為什麼是120。「所以他們一步步進行，但當他們一步步進行時，實際上得出了真正的答案92，而不是他們開始時的答案。如果你問『等等，但你說是120』，他們會說『哦，那是個筆誤，抱歉，正確答案是92』。」

這種表現反映了大型語言模型的本質：「它們不是從第一原理解決問題，而是在輸出的每一步猜測下一個最自然的話語。令人驚訝的是，有時這樣做是有效的，但經常無效。」

為了提高準確性，研究者正在嘗試各種方法。一種是將語言模型連接到更可靠的軟體，「你不會自己進行計算，而是將其外包給Python」。另一種方法是強制模型只產生正確答案，「通過強制模型以這些證明助手語言之一輸出，如果不能編譯，你就把它發送回AI，AI必須再試一次」。

儘管大型語言模型遠未達到能解決大多數數學問題的水平，但它們已經在某些方面展現出價值。陶哲軒分享了個人經驗：「我有一個組合數學問題，嘗試了幾種方法都不奏效，所以作為實驗，我問GPT『你會建議什麼其他技術來解決這個問題？』它給了我10種技術的清單，其中大約5種我已經嘗試過或明顯沒有幫助。但有一種技術我沒有嘗試過，就是對這個特定問題使用產生函數，一旦建議出來，我意識到這是正確的方法，但我錯過了。」

AI輔助證明助手代表了最實用的近期應用。陶哲軒使用GitHub Copilot等工具來加速形式證明的編寫。「寫形式證明是一項非常繁瑣的任務。就像任何真正挑剔的電腦語言一樣——你必須讓語法完全正確。如果你錯過一步，它就不會編譯。」

Copilot能夠預測下一行代碼，「大約20%的時間它實際上會猜到接近正確的東西，然後你可以說我接受這個，說好的」。雖然建議不總是有用，但能顯著加速編寫過程。

這些工具正在快速改進。「現在它們可能——如果證明只有一兩行長，它們可以自動填寫。現在有實驗讓AI建議證明，然後你把它反饋給編譯器，如果編譯錯誤，你就把錯誤消息發送回去。我們開始能夠證明4或5行長的東西——可以用這種方法完成。」

距離自動形式化大型證明還很遙遠，「但它已經是一個有用的工具」。

當AI能處理千題同解：數學研究的規模革命

展望未來，陶哲軒認為AI將在兩個方面徹底改變數學研究的本質。

首先是自動猜想生成。「我認為一個我發現特別令人興奮但還沒有真正成功的方向——希望AI會變得非常擅長生成好的猜想。」結理論的例子只是開始，「只是希望你創建這些巨大的資料集，將它們輸入AI，它們會自動生成許多不同數學對象之間的良好聯繫。我們還不真正知道如何做到這一點，部分原因是我們沒有這些大型資料集，但我認為這是最終可能實現的。」

更根本的變革在於數學研究的規模。「現在因為證明定理是如此痛苦的艱苦過程，我們一次證明一個定理，或者如果你高效的話，可能是兩三個。但有了AI，你可以想像在未來，與其嘗試證明一個問題或解決一個問題，你取一類1000個相似的問題，說『好的，我要告訴你的AI嘗試用這種技術解決這1000個問題』，它會報告回來『哦，我可以用這種技術解決這些問題的35%。這種技術呢？我可以解決這個百分比的問題。如果我結合它們，我可以做這個』。你可以開始探索問題空間，而不是單獨處理每個問題。」

這種大規模探索在傳統數學中要麼完全不可能，要麼需要「數十年的過程，用幾十篇論文慢慢弄清楚你可以和不能用各種技術做什麼。但有了這些工具，你真的可以開始以真正前所未有的規模進行數學研究」。

陶哲軒強調，這種變革不會取代傳統數學方法。「我們仍然會用老式方法證明定理。事實上，我們必須這樣做，因為如果我們自己不知道如何做這些事情，就無法指導這些AI。但我們將能夠做很多現在無法做的事情。」

這種人機協作的未來已經在形式化數學中展現雛形。傳統數學合作受限於信任問題，但形式化環境中「你可以與素未謀面的人協作」，因為所有貢獻都經過自動驗證。這種新的協作模式可能催生出規模空前的數學研究項目。

陶哲軒最後總結：「未來將會非常令人興奮。」他預期AI工具將使數學家能夠探索比以往任何時候都更廣闊的數學領域，但這需要數學家掌握新的技能和工具。對於在場的年輕數學天才們來說，這既是挑戰也是機遇——他們將成為第一代真正與AI協作進行數學研究的數學家。

這場50分鐘的演講，不僅回顧了機器輔助數學的千年歷史，更為我們描繪了一個AI與人類數學家深度協作的未來圖景。從羅馬算盤到現代AI，數學工具的演進從未停止，而我們正站在下一個重大突破的門檻上。正如陶哲軒所說，真正的革命，才剛剛開始。