陶哲軒：數學需要一種「策略語言」，不只是證明語言

本文整理自《Dwarkesh Podcast》2026 年 3 月播出的單集。

{{< youtube Q8Fkpi18QXU >}}

{{< spotify "episode/24xF8YGra2w3HXZYbhgVKU" >}}

{{< apple-podcast "tw/podcast/terence-tao-kepler-newton-and-the-true/id1516093381?i=1000756353875" >}}

---

如果 AI 證出了黎曼猜想，我們能看懂嗎？

假設明天有一個 AI 丟出了三千行 Lean 程式碼，宣稱這是黎曼猜想的證明。Lean 驗證器確認每一步推導都正確。那我們算是「理解」了黎曼猜想嗎？

這是 Dwarkesh Patel 在訪談中拋給陶哲軒（Terence Tao）的問題。陶哲軒是 UCLA 數學教授、2006 年費爾茲獎得主，也是目前全球最活躍地將 AI 整合進數學研究的頂尖數學家之一。他的回答比多數人預期的樂觀：他認為一旦我們擁有了證明的「成品」，要從中提取理解其實沒有想像中那麼難。

他舉了一個正在發生的例子。在厄多斯問題計畫中，AI 產生了一個證明，輸出了三千行程式碼。這三千行程式碼本身確實難以閱讀。但接下來發生的事情很有意思：其他人用另一個 AI 去摘要這個證明，把它濃縮成人類可讀的幾頁文字。還有人根據摘要寫出了自己的版本，用更傳統的數學語言重新表述。這個「後處理」的過程，讓原本不透明的機器證明變得可以被人類消化。

這就是 Lean 這類形式化證明工具的一個常被忽略的優勢。Lean 把證明拆成一連串的原子步驟，每一步都可以被單獨檢視。當你讀一篇人類寫的數學論文時，作者有時不會告訴你哪些步驟是關鍵的、哪些只是例行公事。但在 Lean 程式碼裡，你可以把任何一個引理（lemma）單獨拿出來研究。陶哲軒描述他的審閱過程：看到某個引理，他可以判斷「這看起來很標準，應該沒什麼特別的」，但另一個引理「我沒見過這種做法，這個似乎是整個論證的關鍵」。這種「消融分析」（ablation）的方法，讓數學家可以從一個龐大的證明中辨識出真正的新概念。

證明可以形式化，但策略還不行

Lean 解決了一個重要問題：給定一個數學陳述，AI 可以嘗試用 Lean 來證明它，而 Lean 會毫不留情地告訴你這個證明是對是錯。這個驗證迴路是封閉的、確定的、沒有灰色地帶。這讓強化學習可以被有效地應用在數學證明上，因為獎勵信號是明確的。

但陶哲軒指出，數學家的日常工作中，只有一小部分是在寫證明。更大的部分是在做一些更模糊的事情：決定要研究哪個問題、猜想某個命題可能是真的、評估一個研究方向是否值得投入、判斷某個中間結果是否「有前途」。這些活動涉及的不是演繹邏輯，而是一種混合了直覺、經驗和模式識別的能力。

他把這個差距說得很具體：「Lean 讓我們有了一套形式化的證明語言。但我們還沒有一套形式化的策略語言。」他承認這更像是一個願望而不是一個計畫，因為我們甚至不太清楚這樣的語言應該長什麼樣子。但他指出，擁有一套形式化框架對自動化的推動力有多大，從 Lean 對證明的影響就可以看出來。如果有一套類似的框架能夠描述策略和猜想的合理性，AI 在科學研究中的角色會有質的飛躍。

質數的故事：資料驅動猜想的典範

為了解釋他心目中的「策略語言」應該能處理什麼，陶哲軒講了一個數學史上的經典故事。

十八世紀末，高斯（Carl Friedrich Gauss）做了一件很不數學的事：他計算了前十萬個質數，然後開始找規律。這在當時是革命性的，因為數學家通常是先有理論，再去驗證。高斯反過來，先蒐集資料，再從資料中發現模式。他發現質數的分布不是均勻的，而是越來越稀疏，但稀疏的速度跟自然對數有精確的數學關係。這就是後來被證明的「質數定理」：小於 x 的質數個數大約等於 x 除以 ln(x)。

高斯完全無法證明這個猜想，因為他只有資料，沒有理論工具。但這個猜想啟動了一整個數學分支，叫做解析數論。更重要的是，它建立了一個概念框架：質數的行為可以用統計模型來描述，就好像它們是某個上帝用骰子生成的隨機集合。這個「質數的隨機模型」後來被一次又一次地驗證，它預測的結果跟實際觀察到的幾乎完全吻合。

陶哲軒解釋，這就是為什麼數學家相信「孿生質數猜想」是真的，即使我們還無法證明它。如果質數真的像隨機生成的一樣，那麼基於簡單的機率計算，距離為 2 的質數對（如 11 和 13）應該無窮多次出現。

同樣的推理也是我們相信黎曼猜想為真的原因之一。如果黎曼猜想是錯的，就代表質數裡存在一個我們不知道的隱藏規律，這會動搖整個「質數像隨機數」的概念框架。陶哲軒甚至說，如果黎曼猜想被推翻，密碼學界會立刻放棄所有基於質數的加密系統。理由很簡單：一個未知的規律意味著可能存在更多未知的規律，而這些規律可能被用來破解加密。

我們需要的不是更多證明，而是更多實驗室

高斯對質數的研究方式，本質上是科學的而不是數學的。他蒐集資料、觀察模式、提出假說、用新資料驗證。數學長期以來幾乎完全是理論性的學科，但陶哲軒認為 AI 可能會改變這一點。

他提出了一個很有想像力的構想：如果我們能創造大量的「迷你宇宙」，讓小型 AI 在簡單的數學問題上自己發展策略，我們就能觀察什麼策略有效、什麼沒有。這就像生物學家用果蠅做實驗一樣，不是為了理解果蠅本身，而是為了從大量實驗中提取普遍性的原理。陶哲軒提到，已經有人在研究「能做十位數乘法的最小神經網路是什麼」，這類實驗看起來微不足道，但可能揭示關於學習和推理的深層規律。

但要讓這樣的研究有效運作，就需要一套方法來評估 AI 產生的策略和猜想是否「好」。目前這個評估完全依賴人類專家的判斷和時間的考驗。如果有一套半形式化的框架能做到這件事，陶哲軒認為，AI 在科學中的角色就會從「快速但笨拙的試錯者」升級為「策略性的合作夥伴」。

但他也清楚地警告了一個風險：任何這樣的框架必須是防作弊的。強化學習非常擅長找到系統中的後門和漏洞。如果評估框架有任何可以被利用的弱點，AI 會學會如何騙過框架而不是真正做好研究。這跟 Lean 驗證器的設計哲學一樣：不能有任何捷徑可以繞過驗證而得到「已證明」的標籤。

未來的數學家可能是證明的「考古學家」

陶哲軒描繪了一個很有趣的未來圖景。他說，未來可能會有一整個數學家的職業群體，專門做的事情是：拿到 AI 產生的巨大 Lean 證明，然後像考古學家一樣，去挖掘其中真正重要的新概念。他們可能會對證明做「消融實驗」，嘗試移除某些步驟，看看哪些拿掉了證明就會垮、哪些只是冗餘。他們可能會用其他 AI 來重構證明，讓它變得更優雅。他們甚至可能用 AI 來評分不同版本的證明，看哪個「更好」。

寫論文過去是數學家最耗時的工作，所以人們只在萬事確認之後才動筆，而且只會寫一個版本。重構論文太痛苦了，沒有人想做。但現在，AI 工具已經大幅降低了改寫的成本。一個雜亂的 Lean 證明本身可能不好懂，但別人可以快速產生各種不同的改寫版本、摘要版本、給不同受眾的版本。數學知識的「傳播」將不再受限於原作者的寫作能力。

我的觀察：形式化是 AI 在數學領域的護城河

為什麼 AI 在數學證明上的進展比在其他科學領域快得多？我認為陶哲軒這次訪談揭示了一個關鍵原因：數學有 Lean。

Lean 提供了一個封閉的驗證迴路。AI 產生一個證明，Lean 馬上告訴你對不對。這個回饋是即時的、確定的、完全客觀的。相比之下，在生物學或社會科學中，驗證一個假說可能需要幾個月甚至幾年的實驗。這就是為什麼強化學習在數學證明上特別有效：獎勵信號清晰且即時。

但陶哲軒的洞察是，證明只是數學研究的一部分，甚至可能不是最重要的部分。真正推動數學前進的是策略、直覺、猜想和方向感。這些目前沒有形式化的方法，所以也沒有辦法讓 AI 用強化學習來優化。一旦有人成功建立了「策略的 Lean」，AI 在科學領域的能力可能會有一次根本性的躍升。

這也是為什麼我認為，AI 對科學的影響不會是漸進式的，而是會有「台階式」的跳躍。每一次有人為某個科學領域建立了可靠的自動驗證機制，AI 在那個領域的能力就會突然大幅提升。下一個台階在哪裡？也許就在陶哲軒所說的「策略語言」上。