數學界的GitHub時代：當AI遇上千年證明傳統

2024年11月，被譽為「數學界莫札特」的菲爾茲獎得主陶哲軒，與合作者們解決了一個困擾數學界多年的難題——Polynomial Freiman-Ruzsa猜想。但真正讓數學界震驚的，不是這個證明本身，而是接下來發生的事：陶哲軒立即決定將這個證明「搬上網路」，用一種叫做Lean的程式語言重新撰寫，讓電腦能夠自動驗證每一個步驟。

更令人驚訝的是速度。這個原本需要數個月才能完成的形式化過程，在20個來自世界各地的數學家與程式設計師協作下，僅用了3週就完成了。這群人透過GitHub般的協作平台，像軟體工程師開發程式一樣，分工合作、即時溝通，共同完成了一項數學史上的創舉。

什麼是Polynomial Freiman-Ruzsa猜想？

要理解這個猜想的重要性，我們先從一個簡單的數學遊戲開始。想像你有一袋彈珠，每顆彈珠上都標記著不同的數字。現在，你隨機取出兩顆彈珠，把它們的數字相加，會得到一個新的數字。如果你反覆進行這個「取兩顆、相加」的動作，你會發現一件有趣的事：如果原本的彈珠數字之間有某種規律性，那麼相加後的結果也會呈現某種可預測的模式。

Polynomial Freiman-Ruzsa猜想要解決的，就是這種「規律性傳遞」的數學問題。具體來說，如果你有一組數字，當你把其中任意兩個相加時，得到的新數字集合並沒有變得太大（也就是說，很多相加的結果會重複），那麼這組原始數字本身必定具有某種結構性——它們要嘛像等差數列一樣有規律間隔，要嘛可以用多項式來描述其規律。

這個猜想的深層意義在於：它揭示了「局部的可預測性」如何反映「整體的結構性」。就像你觀察一個城市的交通流量，如果發現某些路段的車流變化很有規律，你就能推測這個城市的道路規劃可能有某種整體性的設計邏輯。在數學上，這種從局部性質推導整體結構的能力，對於理解更複雜的數學系統具有重要意義。

從孤島到協作：數學研究的千年傳統

長久以來，數學研究一直是一個高度個人化的領域。與物理學的大型粒子對撞機實驗，或生物學的人類基因組計畫不同，數學家習慣獨自在書桌前思考，頂多與少數幾個同事討論。陶哲軒在牛津大學的演講中坦言：「數學家很難大規模協作，也許5個人還可以一起工作，但如果要20個人合作，你必須信任所有人的數學能力，這實際上是一個巨大的瓶頸。」

這種協作困難的根源在於數學的特殊性質。一個數學證明就像一座精密的邏輯大廈，每一個步驟都必須完全正確，任何微小的錯誤都可能導致整個論證崩塌。因此，當多人協作時，每個人都必須仔細檢驗其他人的工作，這不僅耗時，更需要極高的互信基礎。

相比之下，天文學早就有了業餘天文愛好者發現彗星的傳統，生物學也有公民科學家協助辨識蝴蝶物種的計畫。但在數學領域，幾乎沒有「公民數學」的概念。業餘愛好者的貢獻往往因為缺乏足夠的技術背景而無法達到專業水準，而專業數學家也沒有有效的工具來整合這些分散的力量。

傳統的學術發表體系更加深了這種孤立。數學家的學術聲望主要建立在期刊論文的數量和影響力上，而期刊通常只認可完整的、由少數作者完成的研究成果。如果有人貢獻了10,000行程式碼到一個包含100個不同數學結果的GitHub專案，這種貢獻很難在現有的評估體系中得到應有的認可。

形式化證明：數學的新語言

改變這一切的關鍵技術叫做「證明助手」（Proof Assistants），其中最著名的是一種名為Lean的程式語言。與一般程式語言設計來執行任務不同，Lean專門用來驗證數學陳述的正確性——它像一個極其嚴格的數學老師，會檢查證明中的每一個邏輯步驟。

這種形式化驗證的概念並不新穎。早在1970年代，數學家就開始嘗試用電腦來驗證著名的四色定理，但當時的形式化過程往往比原始證明還要困難數倍。陶哲軒展示了一個令人印象深刻的時間表：四色定理在1970年代被證明，但直到2000年代才完成形式化；複雜的Kepler猜想在1998年被證明，作者Thomas Hales原本預計需要20年來完成形式化，最終花了12年才完成。

但時代正在改變。近年來，形式化證明的速度大幅提升。數學家Peter Scholze在2020年提出的極其困難的液體張量實驗（Liquid Tensor Experiment），只用了18個月就完成了形式化。而陶哲軒的Polynomial Freiman-Ruzsa猜想，更是創下了從證明完成到形式化驗證僅需3週的紀錄。

這種加速來自於多個因素的結合。首先是軟體工具的進步，Lean等現代證明助手變得更加人性化。其次是協作方式的創新，數學家們開始採用軟體工程中的版本控制和專案管理工具，讓多人能夠同時在同一個證明上工作而不會產生衝突。

最重要的是，形式化證明降低了協作的信任門檻。正如陶哲軒所說：「因為程式語言會檢查每個人上傳的內容是否正確，你不需要像純人類協作那樣的高度信任。」這意味著即使是不同專業背景的人，甚至是程式設計師而非專業數學家，都能在大型數學專案中發揮作用。

AI：數學協作的新夥伴

就在形式化證明技術日趨成熟的同時，人工智慧也開始在數學領域展現驚人的潛力。但陶哲軒對AI有著清醒的認識：「AI本質上是一個猜測機器，它會嘗試給出接近正確答案的回答，但它並不真正理解自己在做什麼。」

這種「猜測機器」的特性在數學應用中既是優勢也是風險。陶哲軒展示了GPT-4的兩個截然不同的表現：一方面，它能夠完美解決複雜的國際數學奧林匹亞問題，給出步驟清晰、邏輯嚴密的完整證明；另一方面，它在計算簡單的算術題「7×4+8×8」時，卻會先猜答案是120，然後在解釋步驟時得出92，最後還辯稱最初的120是「打字錯誤」。

「這就像學生在黑板上解題，」陶哲軒比喻說，「它模糊地記住了一些乘法表，但基本上是在即興發揮。」這種不可預測性使得AI在需要絕對正確性的應用中存在風險，但在數學研究中，這個問題有了優雅的解決方案：形式化驗證。

在陶哲軒的形式化專案中，GitHub Copilot這樣的AI工具已經開始發揮作用。當他需要證明一個關於熵的技術性陳述時，Copilot自動建議了一行Lean程式碼，雖然建議的第一行有錯誤，但第二行是正確的，直接解決了問題。這展現了AI與形式化證明結合的強大潛力：AI負責創造性地提出解決方案，而形式化系統負責嚴格驗證這些方案的正確性。

陶哲軒預測，未來的數學研究將會是這樣的場景：數學家對AI口述證明思路，就像解釋給學生聽一樣，AI會即時嘗試將每個步驟形式化，如果成功就繼續，如果失敗就提出問題，雙方不斷對話直到完成完整的形式化證明。這種方式不僅比傳統數學寫作更快，也更加可靠。

AI重塑科學發現的模式

AI對數學的影響只是更大變革的一部分。在科學研究的許多領域，AI正在從根本上改變研究的效率和方式。陶哲軒用「消防水管」的比喻來形容這種變化：傳統科學研究像是有限流量的水龍頭，能產生一定量的可靠結果，但AI就像一個巨大的消防水管，能產生大量的輸出，雖然其中很多是「不可飲用的」，但如果配上適當的過濾系統，最終能獲得比以往多得多的有用結果。

在藥物開發領域，這種變化已經開始顯現。傳統的藥物發現過程需要先設計候選化合物，然後進行漫長而昂貴的臨床試驗，許多藥物在試驗過程中失敗，整個過程可能耗時十年以上，成本高達數十億美元。AI的介入主要在於大幅縮減需要測試的候選化合物數量。透過分析現有的蛋白質結構和臨床試驗資料，AI可以預測哪些化合物最有可能成功，將需要測試的候選藥物從100個減少到10個，但後續的臨床試驗仍然是必要的安全保障。

材料科學是另一個受益領域。尋找室溫超導體一直是物理學的「聖杯」，研究者們嘗試了各種材料組合，通常以失敗告終，有時甚至會發布樂觀的研究結果但最終仍被證明無效。AI可以在實際合成之前預測材料的性質，大幅減少需要在實驗室中測試的材料種類。

氣候科學的變化更加戲劇性。傳統的氣候模型需要將地球分割成極小的網格，然後在超級電腦上運行數月才能預測未來20年的氣候變化。AI訓練在大量現有模擬資料上後，可以在幾小時內完成同樣精度的預測，速度提升可達10,000倍。這種加速使得科學家能夠運行成千上萬種情境，而不是像聯合國氣候變化專門委員會(IPCC)報告中那樣只能提供三四種情境預測。

在極端天氣預測方面，AI甚至已經開始超越傳統方法。研究團隊訓練AI系統預測颶風登陸位置，在某些情況下比國家氣象局的預報更加準確。這種能力對於災害預警和應急準備具有重要意義。

學術體系的重構迫在眉睫

這些技術變革正在對傳統的學術體系產生深刻衝擊。陶哲軒坦言，數學的學術發表體系已經開始出現問題：論文變得越來越長，找到合適的審稿人越來越困難，而審稿又是數學家們無償提供的服務。當論文的技術複雜性超過人類審稿人的合理負擔時，形式化驗證可能成為必要的補充。

未來的學術評估體系必須適應這種新的協作模式。一個貢獻了10,000行程式碼到大型形式化專案的研究者，其貢獻價值可能不亞於發表一篇傳統期刊論文，但現有的評估體系很難量化這種貢獻。資助機構和大學需要開發新的方法來衡量和認可這些多樣化的學術產出。

數學研究本身也將變得更加專業化。陶哲軒預測，未來可能會有專門的「數學專案經理」，他們不一定要親自完成低層次的證明工作，但擅長組織人員、分解問題，並知道如何將合適的任務分配給合適的人。這種分工類似於軟體開發行業的演進：50年前程式設計師需要獨自完成整個軟體，現在則有了架構師、前端工程師、後端工程師、測試工程師等不同專業角色。

這種變化也將為更多人參與數學研究創造機會。在陶哲軒的形式化專案中，許多貢獻者並非專業數學家，而是有程式設計背景和本科數學基礎的技術人員。他們能夠處理那些邏輯清晰但技術性較強的證明步驟，釋放專業數學家去處理更具創造性的概念工作。

跨學科協作也將變得更加容易。AI可以充當不同領域之間的「翻譯器」，讓數學家與生物學家、物理學家或經濟學家更容易溝通。陶哲軒提到了一些已經出現的多模態生態系統資料庫，來自不同科學領域的研究者在同一個平台上輸入資料，創造出更全面的研究視角。

開放協作與商業競爭的新平衡

然而，這種學術研究的變革正在與商業利益產生複雜的互動。在AI領域，私人企業擁有的資源已經遠超學術機構。正如陶哲軒所觀察的，「私人產業的資源數量級超過學術界，這種情況短期內不會改變，部分原因是私人部門看到了這項技術的巨大潛力。」

今年1月，Google DeepMind發布了AlphaGeometry，這個AI系統能夠解決國際數學奧林匹亞的幾何問題，達到了金牌水準。雖然這個突破主要限於幾何領域（因為幾何問題在數學上屬於「可判定理論」，存在理論上的演算法解），但它展示了商業實驗室在數學AI方面的快速進展。

這種商業化趨勢帶來了新的挑戰。許多最先進的AI模型都是閉源的，這與科學研究的開放傳統形成了張力。學術界需要找到方法來平衡開放協作與商業創新的關係。

陶哲軒建議，政府和學術機構可以專注於那些商業公司較少關注的領域：建立標準化的模型和資料集，創建開源工具，組織競賽來推動創新，以及開發更加輕量級的模型，使其能夠在普通實驗室的電腦上運行，而不需要企業級的計算資源。

競賽特別重要，因為它們能夠量化技術進步。陶哲軒正在參與一項由XTX資助的AI數學競賽，目標是看AI是否能解決只有少數頂尖高中生能夠完美解決的國際數學奧林匹亞問題。這種競賽不僅能推動技術發展，也為評估不同方法的實際效果提供了客觀標準。

重新定義智能的邊界

在這場技術革命中，最深刻的變化可能是我們對「智能」本身的理解。陶哲軒指出，AI研究實際上更多的是在揭示「人類的愚蠢」而不是創造「人工智慧」。許多我們認為需要高度智慧的任務，比如對話、寫作、甚至解決複雜的數學問題，實際上可以透過大規模的模式識別來實現。

「AI告訴我們，像我現在這樣與你對話，基本上就是在預測下一個詞，」陶哲軒說，「這是一個複雜的自動完成過程，就像在手機上反覆按自動完成按鈕，通常會產生垃圾，但達到某個臨界點後，實際上變得相當連貫。」

這種認識正在改變我們對人類認知的理解。許多我們認為需要深度思考的活動，實際上更多依賴直覺和模式識別。相反，一些看似簡單的任務，比如精確的數值計算，對AI來說反而更困難，因為這需要的是算法式的精確性而不是統計模式的近似。

在數學領域，這種認識正在推動研究方式的根本性改變。與其讓人類數學家同時承擔概念創新和技術驗證的雙重負擔，未來的模式可能是讓人類專注於創造性思維和直覺洞察，而將邏輯驗證和技術計算交給AI和形式化系統。

三十年後的數學世界

當被問及如果負責一個數學系的30年發展規劃時，陶哲軒的回答揭示了他對未來的深思熟慮。他強調最重要的是培養「對變化開放」的教師和研究者，因為技術發展的速度使得任何具體的技能預測都可能過時。

他預見了「大數學」時代的到來，類似於物理學和生物學已經存在的大型協作專案。數學研究將不再是個人或小團體的專利，而將演變為涉及數百人的國際合作項目。這些專案將整合專業數學家、程式設計師、AI系統，以及來自其他學科的專家。

在這個新世界中，「公民數學」將成為現實。業餘愛好者將能夠在專業指導下，為重大數學專案做出有意義的貢獻。形式化驗證系統將確保這些貢獻的品質，而不再需要依賴傳統的權威和聲望體系。

教育也將發生根本性改變。傳統的數學教育往往在概念理解和技術計算之間搖擺，學生要麼學到模糊的概念但不會計算，要麼學會計算但不理解概念。在AI時代，技術計算將主要由機器完成，數學教育可以更多地專注於培養概念思維和問題解決能力。

結語：合作超越競爭

陶哲軒的演講最終傳達了一個關於科學未來的重要訊息：雖然AI技術的發展帶來了前所未有的機遇，但真正的突破將來自於合作而不是競爭。無論是學術界與產業界的合作，還是不同學科之間的協作，又或是人類智慧與人工智慧的結合，未來的科學發現將越來越依賴於開放、透明、協作的研究模式。

數學界正在經歷的變革，可能預示著整個科學研究的未來。當證明可以被形式化驗證，當AI可以加速假設的產生和測試，當全球的研究者可以像軟體工程師一樣協作時，我們正在見證科學方法本身的演進。

這不是技術取代人類的故事，而是技術放大人類能力的故事。正如陶哲軒所說：「我們只有一個運作的智能模型，直到最近才有了一個半。」隨著這個「一個半」不斷發展，我們對智能、創造力和科學發現的理解也在深化。

在這個數學界的GitHub時代，每一個證明都可能成為全球協作的起點，每一個猜想都可能在AI的協助下得到驗證，每一個發現都將為整個人類知識體系做出貢獻。這就是陶哲軒所描繪的未來：一個更加開放、協作、高效的科學研究新時代。