關注模型

改變視角真的很重要

無限：假設是球形的奶牛

陶哲軒：一個很好的例子是數學中的塞邁雷迪定理，于1970年代得以證明，它涉及在一組數字集合中尋找某種類型的模式，即等差數列，例如3、5、7或10、15、20。

塞邁雷迪證明了，對于任何足夠大的數字集合，即正密度集合，都包含有任意長度的等差數列。

例如，奇數集合的密度為1/2，則其中包含任意長度的等差數列，因為其實奇數集合相當結構化，我可以輕松找到像11、13、15、17這個等差數列。

塞邁雷迪定理也同樣適用于隨機集合。

如果我取一組奇數集合，然后拋擲一枚硬幣，只保留擲出正面的數字，隨機去掉一半的數，將得到一個完全沒有模式的集合。

但由于隨機波動，你仍然會在這個集合中找到許多等差數列。

Q：能否證明在隨機集合中存在任意長度的等差數列？

陶哲軒： 可以的，比如說無限猴子定理。如果一個房間內有無數會使用打字機的猴子，讓它們隨機打字，其中一只一定會打出完整的《哈姆雷特》劇本或任何其他有限的文本字符串。

這需要相當長的時間，但只要是無限，那么它終會發生。

所以如果你取一個無限的數字串或其他，最終都會呈現出你想要的任何有限模式，只是需要很長時間，等差數列也是如此。

Q：人類應當如何看待無限呢？

陶哲軒：可以把無限視作一個有限數的抽象，而它沒有界限。但現實生活中其實沒有真正的無限，但你可以假設，比如如果我想有多少錢就有多少錢，想走多快就可以走多快。

數學家就是利用數學將這種形式主義理想化，不是極大或極小，而是無限或零。此時，數學將變得簡潔。

在物理學中，我們常常開玩笑地說，假設是球形的奶牛，現實世界中的問題總會受現實世界影響，但你可以理想化，將某些東西送到無限，某些東西送到零，數學就變得容易處理。

Lex Fridman：我想知道使用無窮大有多頻繁地迫使我們偏離現實世界的物理規律。

陶哲軒：這里存在很多陷阱。我們在本科數學課上花費了很多時間教授分析學，但分析學是關于如何取極限，例如a+b恒等于b+a，有限項可以交換，但無限項時，如果有一個收斂于某值的級數，重新排列，它將突然收斂于另一個值，則會出現錯誤。

所以當使用無限時，必須引入ε和δ，以及特定的推理方式，以避免類似錯誤。

近年來，人們開始對無限極限下成立的結果進行有限化，也就是說，某件事最終將會成真，但無法確定具體時間和速率。

那么如果我沒有無限只猴子，而是有限只，我需要等待多久才能看到《哈姆雷特》出來呢？

這是一個定量問題，可以用純粹有限的方法解決，或者利用你的有限直覺。

結果表明，生成的文本長度將呈指數級增長，這也就是為什么你永遠看不到猴子寫出《哈姆雷特》的原因。也許你能看到猴子們寫出了一個包含四個字母的單詞，但僅此而已。

所以我發現，當把一個無限的陳述有限化，它就會變得直觀得多，也就沒那么奇怪了。當然缺點是有限化群要混亂得多，而無限化群在幾十年前就得以發現，后來人們才將其有限化。

數學關注模型，物理解釋模型

Q：數學與物理學之間，在理解和看待世界的方式上有什么區別？

陶哲軒：我認為科學通常是三者之間的相互作用：現實世界、我們對現實世界的觀察，以及我們認為世界如何運作的心理模型。

我們無法直接接觸現實，我們只擁有不完整且存在很多誤差的觀測結果。

當我們想要預測的時候，例如預測天氣，我們只有簡化的模型，有時也只能給出不切實際的假設，就像球形奶牛。

這就是數學模型，數學關注的是模型，而科學收集觀察結果并提出解釋模型。

數學讓我們停留在模型內部，并詢問模型帶來的后果，以及對未來會做出什么預測、是否符合過去的觀測數據。而這期間肯定存在共生關系。

數學與其他學科相比，是很不同尋常的，因為數學始于假設，比如模型的公理和模型的結論。

但幾乎其它學科中，都是始于結論，比如我想建一座橋，然后去找到通往那個結果的路徑。這當中很少存在假設，當然推理小說除外。

我們生活中所做的絕大多數事情都是由結論驅動的，包括物理學和科學，例如“這顆小行星會去向哪里？”、“明天的天氣會是怎樣？”，但數學卻是從公理出發。

Q：物理學中存在理論與實驗之間的張力，你認為發現有關現實的真正新穎思想的強有力方法是什么？

陶哲軒：需要同時擁有自上而下和自下而上，這是所有事物之間真正的互動關系。隨著時間推移，觀察、理論和建模都應該更接近現實，即使一開始它們總是相距甚遠，只需要擁有其中一個就能弄清楚將另一個推向何方。

因此，如果你的模型預測的是實驗未捕捉到的異常情況，它將會告訴實驗者去哪里查找更多數據來優化模型，這需要反復操作。

在數學本身中，也存在理論和實驗的部分。只是最近，理論幾乎完全占據主導地位。99%的數學是理論數學，實驗數學非常少。因為假如他們想要研究素數或者其它，可以直接利用計算機生成大型數據集。

就像高斯發現了一個猜想，數論中最基本的素數定理，它預測了一百萬乃至一萬億可以有多少個素數。這個問題上，他主要靠自己計算，但也雇傭了人類計算員，用以計算前100000個素數并制作表格，做出預測。

這是實驗數學的一個早期例子，但顯然理論數學要成功得多，也是直到最近，做一些復雜的數學計算才變得可行。但即便我們現在擁有強大的計算機，也只有一部分數學事物可以通過數值探索。

比如有一種叫做組合爆炸的東西，當你想研究1到1000的所有可能子集，子集數量將會是2 的1000次方，這比目前的任何計算機可枚舉的都要大得多。所以有些數學問題無法直接通過暴力計算來解決。

國際象棋則是另一個著名的例子。關于國際象棋排列的數量，我們至今無法用計算機完全解決，但我們現在有AI，它們不會探索博弈樹中的每個位置，而是尋求近似值。

事實上人們現在就正在使用這種國際象棋引擎來做實驗性國際象棋。他們正在重新審視古老的國際象棋理論，例如傳統的經典開局，也許并不是最優解，他們希望用國際象棋引擎來實現改進。

我希望數學在未來會有更大的實驗成分，也許將由AI驅動。

數學的不合理但有效

Lex Fridman：你提到了柏拉圖的洞穴寓言。如果人們不知道洞穴是人們觀察現實的影子，而不是現實本身，并且他們相信他們所觀察到的就是現實——從某種意義上說，這是數學家和也許所有人類都在做的事情，即觀察現實的影子——我們有可能真正接觸到現實嗎？

陶哲軒：這當中存在三個本體論的東西，分別是實際的現實、我們的觀察和我們的模型，嚴格來說它們彼此不同，而我認為它們將永遠不同。但它們會隨著時間逐漸靠近，但在靠近的過程中必須舍棄掉你最初的直覺。

例如在天文學中，最初人們認為世界模型是平的，因為它看起來很平，且很大。而宇宙的其余部分，即天空，則看起來很小。所以當你從模型出發，它實際上與現實相去甚遠，但它又符合當下你的觀察結論。

但隨著時間推移和越來越多的觀察，模型將更接近現實，我們也會意識到地球是圓的，它在旋轉，并圍繞著太陽系運行，而太陽系圍繞著銀河系運行，而宇宙在膨脹，膨脹本身也在加速膨脹……但事實上就在今年，我們發現宇宙的加速也是非恒定的，由于暗物質或暗能量這類東西的存在。

我們有一個數據擬合相當好的模型，在某種程度上可以解釋它。該模型只有幾個你必須指定的參數。但人們會說，那是捏造因子，有足夠的捏造因子，你就可以解釋任何事情。可是數學的觀點是，希望模型中的參數要比觀測數據集中的數據點少。

如果一個模型有10個參數，可以解釋10個觀測結果，該模型將完全無用，這叫做過擬合。而如果你的模型只有兩個參數，卻解釋了1萬億個觀測結果，這就是暗物質模型，我認為它有14個參數，可以解決天文學家擁有的PB級數據。

所以你可以把一個物理數學理論看作是對宇宙的一種數據壓縮，即把這些PB級數據壓縮為一個可以用五頁紙描述的模型，并指定一定數量的參數，如果它能以合理的精度擬合幾乎所有的觀測結果，那么壓縮越多，你的理論就越好。

愛因斯坦說過這樣一句話：“宇宙中最難以理解的事情是它是可理解的。”，這就是數學的不合理但有效。

實際上這里有一些可能的數學解釋，比如數學中有一種叫做普適性的現象。許多宏觀尺度上的復雜系統都是從大量微觀尺度上的微小相互作用中產生，而由于組合爆炸，你會認為宏觀尺度的方程一定比微觀尺度的方程指數級復雜。

如果要完全精確地求解，比如模擬一盒空氣中的所有原子，就像阿伏伽德羅常數這將會是巨大的，如果你真的試圖跟蹤每一個粒子，這將是荒謬的。

但某些定律只在微觀尺度上涌現，幾乎不依賴于宏觀尺度上發生的事情，或者只依賴于非常少的幾個參數。所以，如果要模擬盒子里包含萬億粒子的氣體，只需要知道它的溫度、壓力、體積以及五六個參數，就可以模擬10^23或任何數量的粒子的所有信息。

因此，我們無法在數學上理解普適性，但存在一些可以幫助我們理解普適性發生原因的玩具模型，例如中心極限定理就解釋了為什么鐘形曲線在自然界中無處不在，那么多事物都是高斯分布。

現在甚至還有一個攜帶鐘形曲線的模因，甚至模因也具有普適性。

如果你愿意，你可以選擇元，但存在許多過程，比如選取很多獨立的隨機變量，以各種方式將它們平均在一起，取簡單平均或更復雜的平均，我們就可以在各種情況下證明高斯曲線的出現。

但如果你有許多不同的輸入，且它們之間存在某種系統關聯，則可能得不到鐘形曲線，所以普適性并不是100%可靠。

全球金融危機就是這方面的一個著名例子。人們認為抵押貸款違約的行為存在高斯曲線，如果在擁有抵押貸款的十萬美國人中，詢問違約比例，如果一切都是去相關的，將會生成漂亮的鐘形曲線，然后你可以用期權和衍生品管理風險。

但如果經濟中存在系統性沖擊，推動所有人同時違約，那將是非常反高斯的行為，這就是2008年沒有被充分考慮進去的后果。

我認為，現在人們更多地意識到，系統性風險實際上是一個更大的問題，模型很漂亮，但它可能不匹配現實。所以研究模型行為的數學非常重要，但也需要科學來驗證它何時符合現實，何時不符合。兩者都被需要。

而數學可以提供幫助，因為像中心極限定理就會告訴你，某些假設的輸入之間如果不相關，那么你就會擁有高斯行為。它也會告訴你到哪里去尋找模型中的弱點。

所以如果你理解中心極限定理，就可以使用高斯行為或其它來模擬違約風險，如果你受過數學訓練，你就會尋求輸入之間的系統相關性，并詢問經濟學家這樣存在多大的風險，然后你就可以繼續了。所以在科學和數學之間總是存在這種協同作用。

Q：是否存在一種可以將不同領域的數學連接起來的底層結構？

陶哲軒：肯定存在相互聯系的線索，數學的很多進展都來自于將兩個先前沒有聯系的數學領域聯系起來。一個古老的例子是幾何和數論。在古希臘時代，它們并不被認為是相關的，直到笛卡爾意識到并發展了解析幾何，可以用兩個實數來參數化幾何對象平面。幾何問題最終可以轉化為數字問題。

當然今天這兩個領域已經統一了，類似的過程也在數學中反復上演，代數和幾何曾是分開的，現在又有了代數幾何。

我認為數學家也有各種風格，就像刺猬和狐貍，狐貍知道很多事但都只懂一點，而刺猬只知道一件事但知道得很深。理想的數學家合作就需要多樣性，讓一只狐貍與多只刺猬合作，或者反之亦然。

我主要認為自己是一只狐貍，我很喜歡套利這個金融說法，學習一個領域是如何運作的，了解該領域的技巧，然后去到另一個不相關領域，但我可以自行調整這些技巧，看到領域之間的聯系。

所以還存在許多比我研究更深的科學家，他們是真的刺猬，了解一個領域的一切，且在那個領域更快、更有效，而我可以給他們提供額外的工具。

而兩種思考之間，我更傾向成為狐貍，我喜歡尋找類比、敘述。假如我看到一個領域的結果并且很喜歡，但我不喜歡證明，尤其是它使用了我不是很熟悉的數學類型，我將經常會嘗試用我喜歡的工具重新證明它。

通常我的證明更糟糕，但通過這樣練習，我可以充分明白另一個證明試圖在做些什么。由此我可以對那個領域使用的工具有所理解。這是非常具有探索性的，非常像是在瘋狂的領域里做瘋狂的事情，并且像是在大量重新發明輪子。

刺猬風格也會更學術，你將會非常注重知識，及時了解這個領域的所有進展。了解所有歷史并對每種特定技術的優缺點有很好的理解。你會更依賴計算而不是試圖尋找敘述。當然我也可以那樣做，但始終有其他人在那方面更為擅長。

Q：你是在什么時候意識到數學可以有一種優雅和美感的？

陶哲軒：當我來到普林斯頓讀研究生時，John Conway當時也在那里，他于幾年前去世了。但我記得我參加的最早的研究講座之一，就是Conway關于他的極端證明的報告。

Conway會以一種你通常不會想到的方式思考各種事物，他認為證明本身就占據了某種空間，所以如果你想證明某件事，比如說有無限多個素數，你可以把它們放到不同的軸上。

有些證明是優雅的，有些證明很長，有些證明是初級的。這樣就有了證明空間，且空間本身具有某種形狀。他對形狀的極值點很感興趣，比如在所有證明中，什么是以犧牲其他一切為代價的最短證明？或者什么是最初等的證明？或者其它。

所以他列舉了一些著名定理的例子，然后他會給出他認為是這些定理的極端證明。這真的讓人大開眼界，這不僅是得到一個有趣的結果證明，而且一旦你有了這個證明，試圖用各種方式優化它，證明本身就擁有了一些技巧。

這也影響了我的寫作風格。比如當你做本科數學作業時，你被鼓勵寫下任何有效的證明并交上去，得到一個勾，你就繼續前進。

但如果你希望你的結果真正具有影響力并被人們閱讀，它就不能只是正確的。它也應該讓閱讀成為一種享受，才能有動力推廣到其他事物。

這和許多其他學科一樣，比如像編碼。數學和編碼之間有很多類比。就像你可以用意大利面條式代碼編寫一些東西，它適用于某個任務，又快又臟而且高效。但其實有很多可以寫好代碼的好原則，這樣其他人就可以使用它，并在此基礎上構建，減少錯誤的發生，數學也有類似的事情。

另外還有一種叫做代碼高爾夫的活動，我也覺得它美麗而有趣。人們使用不同的編程語言，來試圖寫出完成特定任務的最短程序。

我甚至相信這里存在一個比賽，不僅可以對程序進行壓力測試，還可以對證明或者不同語言進行測試。也許這是一種不同的符號，用以完成不同的任務。

Lex Fridman：你覺得數學中最美麗或最優雅的方程是什么？歐拉恒等式常被認為是數學中最美麗的方程，你是否在那個方程式中，在歐拉恒等式中找到了美？

陶哲軒：我來說的話，我覺得最吸引人的是不同事物之間的聯系，歐拉恒等式使用了所有的基本常數，這很可愛。但對我來說，指數函數是歐拉引入來測量指數增長的，所以復利或衰減，任何持續增長、持續減少、膨脹或收縮的東西，都可以用指數函數建模。

而π來自圓和旋轉，如果你想轉一根針180度，你需要旋轉π弧度。而i復數表示虛軸上的擺動，對應90度的旋轉，所以是方向上的改變。所以指數函數代表當前方向上的增長和衰減。當你在指數中加入i時，它現在變成與當前位置成直角的運動。

然后歐拉恒等式將告訴你，如果你旋轉一個時間π，你最終會得到另一個方向。它將通過復化和i的旋轉，將所有數學工具統一起來，包含數學、動力學、幾何和復數。

而當你第一次研究任何東西時，你必須測量事物并為它們命名，有時因為模型與現實相去甚遠，也會給錯誤的東西起了好名字，但直到后來你才發現什么是真正重要的東西。

例如在物理學中，E=MC2，其中一件大事就是E，而當亞里士多德首次提出運動定律，然后是伽利略或牛頓能測量質量、加速度、力等等，所以有了著名的牛頓第二運動定律F=ma。因為這些是主要對象，所以它們被賦予理論中的核心位置。

直到后來人們開始分析這些方程，才發現似乎這些量總是守恒的，特別是動量和能量。

而事物是否擁有能量，這并不明顯，能量它不像質量、速度那樣可以直接測量，但隨著時間推移，人們逐漸意識到這實際上是一個非常基本的概念。

哈密頓最終在19世紀將牛頓物理定律重新表述為哈密頓力學，其中能量，也就是哈密頓量是主導對象，一旦你知道如何測量任何系統的哈密頓量，你就能完全描述動力學，即所有狀態會發生什么。

它作為核心角色，起初也并不明顯，而當量子力學出現時，視角的轉變則提供了很大的幫助。

研究量子力學的早期物理學家，他們首先嘗試將牛頓力學融入量子力學，但遇到了很多麻煩，因為一切都是粒子，而我認為它是波，總之結合起來非常奇怪。

如果你問，F=ma的量子版本是什么，這很難回答。但事實證明，在經典力學背后的哈密頓量也是量子力學的關鍵對象，這里也有一個叫做哈密頓算符的對象。它是一種不同類型的對象，是運算符而不是函數，但一旦指定了它，你就指定了整個動力學。

所以這里有一個叫做薛定諤方程的東西，它可以準確地告訴你，一旦你擁有哈密頓量，量子系統將會如何演變。

所以將二者放在一起，看起來是完全不同的對象，一個涉及粒子，一個涉及波。但有了中心性，就可以將很多直覺和事實從經典力學轉移到量子力學。

例如，在經典力學中，有一個叫做諾特定理的東西。每當物理系統中存在對稱性，就有出現守恒定律。所以物理定律是平移不變的。

比如如果我向左移動10步，我會體驗到與初始位置相同的物理定律，這對應動量守恒。而如果我以某個角度轉身，我又將再次體驗到相同的物理定律。這對應角動量守恒。如果我等待10分鐘，我仍然有相同的物理定律，由于存在時間平移不變性，這對應能量守恒定律。

所以在對稱性和守恒之間存在這種基本聯系，這在量子力學中也成立。盡管方程完全不同，但因為它們都源于哈密頓量，哈密頓量控制一切。當每次哈密頓量具有對稱性時，方程就會有一個守恒定律。所以一旦你擁有正確的表述，很多事情都變得清晰起來。

我們無法統一量子力學和廣義相對論，因為我們還沒有弄清楚基本對象是什么，例如我們必須放棄空間和時間的概念，因為這些空間幾乎是歐幾里得類型，只在非常小的尺度上出現量子漲落，從而形成時空泡沫，試圖用笛卡爾坐標xyz解釋是行不通的，但我們還不知道用什么來代替它。我們沒有類似于哈密頓量能組織起一切的類似數學概念。

直覺就在那里，你必須轉移它

Q：你的直覺是否認為存在一個萬物理論，可以找到一個統一廣義相對論和量子力學的語言？

陶哲軒：我相信如此。多年來，物理學的歷史就是統一的歷史，就像數學一樣。例如電和磁是分開的理論，然后麥克斯韋統一了它們。牛頓統一了天體的運動與地球上物體的運動。等等諸如此類，都說明了統一時有發生。

再次回到這個觀察和理論的模型，我們物理學的兩個大理論，廣義相對論和量子力學，現在發展如此之好，加起來涵蓋了我們所能做的所有觀察的99.9%。

你現在要么去研究極其瘋狂的粒子加速器，或者早期宇宙，再或者那些知道很難以測量的東西，才能偏離這兩個理論中的任何一個，直到你真正弄清楚二者如何結合在一起。

但我相信，我們已經這樣做了幾個世紀，我們在以前也已取得一定進展，沒理由我們應該放棄。

Q：您認為您會成為一名發展萬物理論的數學家嗎？

陶哲軒：經常發生的情況是，當物理學家需要一些數學理論時，通常數學家們已經研究出了一些前身理論。

所以當愛因斯坦開始意識到空間是彎曲的，他去找一些數學家詢問彎曲空間理論是否可用，然后他說，他認為黎曼發展了黎曼幾何學，這恰恰是一種空間以各種一般方式彎曲的理論。事實證明，這就是愛因斯坦理論幾乎完全需要的。

這就又回到了數學的不合理的有效性，那些能很好地解釋宇宙的理論，往往也能很好解決具有相同數學對象的數學問題。歸根結底，它們只是組織數據的兩種有效方式。

而弦理論，雖然幾十年來一直保持領先，但我認為它正在慢慢退出歷史舞臺，因為它與實驗并不匹配。

Lex Fridman：當前最大的挑戰之一就是實驗非常困難，因為兩種理論都如此有效，但另一方面，你所談論的不僅是偏離時空，更是進入一些瘋狂的維度，你現在所做的事情，對我們來說，已經距離我們認為地球是平坦的時候相隔甚遠，我們很難用有限的認知來感知那個所謂的現實到底是什么。

陶哲軒：這就是為什么類比如此重要。圓形的地球并不直觀，因為我們被困在其上，但我們對圓形物體以及光的工作原理有相當好的直覺。

實際上，這是一個很好的練習，為了真正弄清楚日食、月相是如何發生的，可以用圓形地球、圓形月亮的模型很輕松地解釋。你可以拿一個籃球、一個高爾夫球和一個光源，自己實際去做這些事情，直覺就在那里，你必須轉移它。

現代科學也許是自身成功的受害者，為了更加準確，需要離最初的直覺越來越遠。因此，對于沒有經歷過科學教育的人來說，這個過程顯得相當可疑，因此我們需要更多科學基礎。

有些科學家做了相當出色的外出推廣工作，但在家里也可以做很多科學的事情。YouTube上有很多視頻，我最近就和Grant Sanderson一起做了一個YouTube視頻，我們討論古希臘人如何能夠測量到月球的距離、到地球的距離，并使用你自己也可以復制的技術，不一定是花哨的太空望遠鏡或令人生畏的數學。

改變視角真的很重要。旅游可以拓寬思維，而這就是智力旅行，你把自己放在古希臘人或者其它時期的人的腦海中，做出球形奶牛的假設，這是數學家所做的，也是一些其他藝術家正在做的。

如果你提出公理，那么數學會讓你遵循這些公理并得出結論，有時你將可以從初始假設中走得很遠。

想象自己是個矢量場

Q：能否從數學的角度解讀廣義相對論，它的那一方面讓你感興趣，對你來說具有挑戰性？

陶哲軒：我研究過一些方程。有一個叫做波映射方程或西格瑪場模型的東西，它并不完全等同于時空引力本身的方程，而是某些可能存在于時空之上的場的方程。

所以愛因斯坦的相對論方程只描述時間和空間本身，但還有其他場存在，比如電磁場、楊-米爾斯場，以及一整套不同的方程。

其中愛因斯坦方程被認為是最非線性和困難的方程之一，但在層次結構中相對較低的，是這個叫做波映射方程的東西。

這是一個波，在任意給定點上都像是被固定在一個球體上。所以我可以想象時空中有許多箭頭，這些箭頭指向不同的方向，像波浪一樣傳播。如果你擺動其中一個箭頭，它會傳播并使所有箭頭移動，這有點像麥田里的麥浪。

我對這個方程的全局正則性問題很感興趣，那么是否可以讓所有能量集中于一點呢？所以我考慮的方程實際上是所謂的臨界方程，它實際上在所有尺度上的行為都大致相同。我勉強證明了，你實際上無法強迫所有能量都集中到一點上，能量必須在此刻稍微分散一點，而一旦它分散一點點，它就會保持正則。

是的，這是在2000年發生的事。所以這其實也是我后來對納維-斯托克斯方程感興趣的部分原因。我開發了一些技術來解決這個問題，所以得出的部分結論是由于球體的曲率，這個問題實際上是非線性的，存在一種非微擾效應。

當你正常觀察它時，它看起來比波動方程的線性效應更大，即使你的能量很小，也很難將其控制。

但我開發了一種叫做規范變換的東西，方程有點像麥浪的演化，它們都在來回彎曲，存在很多運動。但如果想象一下，通過在空間的不同點上，附加小攝像機來穩定流動，這些攝像機試圖以捕捉大部分運動的方式移動，在這種穩定的流動下，流動將會變得線性得多。

我發現了一種可以減少非線性效應量的變換方程，然后我就能夠求解這個方程了。這是我在澳大利亞拜訪我的姨母時，發現的這個變換，當時我試圖理解所有這些場的動力學，但我無法單單用紙筆完成，也沒有足夠的計算機設備來做任何計算機模擬。

所以我最終閉上眼睛，躺在地板上，想象自己實際上是個矢量場，然后來回翻滾，試圖找到如何改變坐標，讓各個方向的事物都能以合理的線性方式運行。

當我這樣做時，我的姨母走進來問道，我在做什么。我回答說，這很復雜。于是姨母說，好吧，你是年輕人，我不多問了。

學會策略性“作弊”

Q：你是如何解決難題的，是否在腦海中經常可視化數學對象、符號？

陶哲軒：有很多的紙和筆。作為一名數學家，我學到的一件事情是，策略性作弊。

數學之美在于你可以隨心所欲地改變規則、改變問題，這是其它任何領域都無法做到的一點。如果你是一名工程師，有人說，在這條河上建造一座橋，你不能說，我想在這里建一座橋或者我想要紙而不是鋼來建造它，但作為數學家，你可以做任何你想要做的事情。

這就像試圖通關一個電腦游戲，其中有無限的作弊碼可用。你可以自行設置，例如有一個很大的維度，我可以先將其設為一，先解決一維問題，因此存在一個主項和一個誤差項，所以我需要做一個球形奶牛假設，假設誤差項為零。

所以當你試圖尋找解決問題的方法，不應該在鐵人模式下進行，讓事情變得最大化困難，更合理的解決方式是，如果有10件事讓你的生活變得困難，你可以先找到其中一個問題并關閉另外九個困難。

這樣你就安裝了九個作弊碼，而如果你安裝了十個作弊碼，那么這個游戲將是微不足道的。當你安裝九個，然后集中解決那一個問題，它將教會你如何解決那個特定的困難，然后你關閉這個，再打開其它問題并依次解決。在你最終學會如何分別解決這10個問題后，再將其中幾個合并處理。

小時候，我看了很多我們文化中的香港動作片，每次遇到打斗畫面，例如英雄會被一百個壞蛋嘍啰包圍，在精心設計的場景下，他一次只會與一個人戰斗，打敗那個人后再繼續前進。正因為如此，他可以打敗他們所有人。

但是，如果這群人更聰明一點，就應該直接蜂擁而上，當然這樣電影效果會很糟糕，但他們會贏。

Q：你通常是使用紙和筆工作嗎？是否會使用計算機和LaTeX工作？

陶哲軒：實際上主要是紙和筆。在我的辦公室里，我有四塊巨大的黑板，有時候只需要把我所知道的關于問題的所有信息都寫在這上面，然后我會坐在沙發上，看著整個東西。

其中有很多繪畫和只有自己能理解的定制涂鴉。黑板的美妙之處在于可以擦除，但現在我也開始越來越多地使用計算機，部分原因是因為AI能執行簡單的編碼工作，讓事情變得更加容易。

以前如果我想要繪制一個中等復雜度的函數，包含一些迭代或其它東西，我必須記住如何設置Python程序、以及循環如何工作并調試它，這需要兩個小時的時間。但現在我可以在10到15分鐘內完成，所以我現在使用越來越多計算機進行簡單的探索。

總有算法來負責將一棵樹和另一棵樹進行匹配

Q：可以描述一下Lean形式化證明編程語言嗎？以及它是如何作為證明助手提供幫助的？

陶哲軒：Lean是一種計算機語言，就像Python和C等標準語言一樣，但在大多數語言中，重點在于產生可執行代碼。代碼行會執行一些操作，例如翻轉比特、讓機器人移動或在互聯網上發送文本等。

而Lean也是可以做到這一點的語言，可作為一個標準的傳統語言運行，但它也能生成證書。像Python這類軟件可能會進行計算并告訴你3+4的答案是7，但Lean不僅可以生成答案，還能生成它是如何得到7的證明，以及其中涉及的所有步驟。

它創建了更為復雜的對象，不僅僅是陳述，而是帶有證明的陳述。每一行代碼都只是將先前的陳述拼湊在一起，然后創建新陳述。

這個想法并不新鮮，它們被稱為證明助手。它們提供語言，讓你可以創建相當復雜精細的數學證明。如果你的編譯器可信，那它們會生成證書，確保你的觀點100%正確，但它們也會讓編譯器變得非常小，并且有多個不同的編譯器可用。

Q：你是否可以描述一下在紙筆上書寫和使用Lean編程語言之間的區別？形式化一個陳述有多難？

陶哲軒：很多數學家都參與了Lean的設計，所以它被設計成單獨的代碼行，類似于數學論證的單獨行。比如你可能想引入一個變量，證明一個矛盾。有很多你可以做的標準操作，理想情況下應該是一一對應的，但實踐中并非如此。

Lean就像向一個極其迂腐的同事解釋一個證明，他會指出，你真的是這個意思嗎？如果這個是零怎么辦？你如何證明這個？而Lean中包含很多自動化功能，可以減少麻煩。

例如，每個數學對象都必須包含一個類型，比如談論X，X是實數、自然數，還是函數或者其它，如果非正式數學，它通常需要有上下文，例如“顯然X是Y和Z之和，Y和Z是實數，那么X也應該是實數。”

Lean可以做很多類似的事情，每隔一段時間它就會說，你能告訴我更多關于這個對象是什么的信息嗎？它是什么類型的對象？所以你必須在哲學層面上思考更多，不僅僅是你正在做的計算，而是每個對象在實際意義上代表什么。

Lex Fridman ：它是使用LLM進行類型推斷嗎？還是可以與實數匹配？

陶哲軒：它使用了更傳統的老式AI。你可以把這些東西都表示成樹，總有算法來負責將一棵樹和另一棵樹進行匹配。每個物體都有歷史可以追溯。

Lean是為可靠性而設計的，所以現代AI沒有被用在里面，它是一個完全不相關的技術。

所以當一個數學家試圖在Lean中編程一個證明時，通常會有這樣一個步驟，比如“好的，我現在想要使用微積分的基本定理來做下一步。”

所以Lean開發者構建了這個龐大的項目mathlib，它是一個包含數萬個有關數學對象有用事實的集合，其中就有微積分基本定理，但你需要找到它，所以現在的很多瓶頸是引理搜索。

你可以有各種專門用于數學引理搜索的搜索引擎，但現在有了這些大型語言模型，你就可以直接詢問它們，例如當我編碼時，我在我的IDE中安裝了GitHub Copilot作為插件，它會掃描我的文本，看到我的需求。

當我需要使用微積分基本定理時，它會提供建議，25%的時間它完全正確，另外10-15%的時間它不完全有效，但足夠接近，然后我會告知它需要修改的地方，它就會生效，然后大約有一半的時間，它給我的是完全的垃圾。但人們開始在上面使用一點點人工智能，主要在自動補全的層面上，你可以輸入證明行的一半，讓它告知你另外一半。

所以我現在估計，將一個證明形式化出來所需的時間和精力大約是寫出來所花費的時間和精力的10倍，它是可行的，但很煩人。

這是它唯一迂腐的地方，但在某些情況下，形式化地做事情實際上更愉快。有一個我形式化了的定理，在最終陳述中存在常數12，12必須貫穿整個證明，所有其它數字都必須與這個最終數字12保持一致，所以我們寫了一篇圍繞著數字12的定理文章。

然后幾周后，有人說可以通過重新處理其中一些步驟，將12改進為11。當這種情況發生在紙筆上時，每改變一個參數，就必須逐行檢查證明的每一行是否仍然有效，并且可能存在一些你沒有意識到的微妙之處，你沒有意識到你在利用12的某些性質，所以一個證明可能在微妙之處崩潰。

所以我們用常數12形式化了這個證明，當新論文出來時，花了我們20個人大約3周時間形式化。然后現在將12更新到11，在Lean里面直接修改就行， 然后運行編譯器，在所擁有的數千行代碼中，90%仍然有效，只有少數幾行標紅。

現在我無法證明這些步驟的正確性，但它立即隔離出哪些步驟你需要改變，你可以跳過所有正常工作的部分，只會有一小部分地方需要你修改。所以在一兩天內，我們就把我們的證明更新到了11。這是一個非常快的過程，比紙筆要順利得多。

由于證明更長，每個單獨的部分更容易閱讀。例如當你拿到一篇數學論文，跳到第27頁，看第6段，這里有一行數學文本，我常常不能立即讀懂它，因為它假設了各種定義，我必須回去去找，也許10頁前定義了這個，證明總是分散在各處，所以你基本上被迫連續閱讀。

它不像小說那樣，可以打開一半開始讀，這里存在很多上下文。但當證明在Lean中時，如果你把光標放在某一行代碼上，那里的每個對象，你都可以讓光標懸停，它會說出這是什么，來自哪里，在哪里被證明。這比翻閱數學論文更容易回溯事物。

所以，Lean真正實現的一件事是，在原子尺度上協作證明，這在過去是無法做到的。所以傳統上，當你想與另一位數學家合作時，要么在黑板前進行真正的互動，要么通過電子郵件或其它方式，但必須進行分段，例如我要完成第3節，你做第4節，但不能真正在同一時間在同一件事上協作工作。

但有了Lean，你就可以嘗試形式化證明某一部分，然后說，我在第67行卡住了，我需要證明這個東西，但它并不完全有效，這是我有麻煩的三行代碼。由于所有上下文都在那里，別人可以說，好的，我知道你需要做什么，你需要應用這個技巧或這個工具。

你可以進行極其原子級別的對話。因為Lean，我可以與世界各地的幾十個人合作，其中大多數人我從未見過面。實際上我也不知道他們在過程中是否可靠，但Lean給了我一份信任證書，這樣我就可以進行無信任數學。

Q：在合作時，解決數學難題的正確方法是什么呢？是分而治之，還是你會專注于某個特定部分，并且正在頭腦風暴？

陶哲軒：首先總是有一個頭腦風暴過程。對于數學研究項目，本質上從一開始，你真的無從下手。它不像一個工程項目，理論已經確立了幾十年，實施才是主要困難。你甚至必須弄清楚什么是正確的路徑。

就像我之前說的“作弊”，回到建橋的類比，首先假設你擁有無限的預算和無限的勞動力，現在你能建這座橋嗎？那現在有無限的預算但只有有限的勞動力，現在你能做到嗎？當然沒有工程師能真正做到這一點，因為他們有固定的要求。

在項目開始你總是會嘗試各種瘋狂的事情，做出所有不切實際的假設，但你計劃稍后再來修正解決。然后你會嘗試看看是否存在一個可能有效的方法框架，并寄希望于將問題分解為更小的子問題，然后你就可以專注于子問題。

有時不同的合作者更擅長處理某些事情。例如我和本·格林的一個定理，叫做格林-陶定理（the Green-Tao theorem）定理。它是一個關于素數包含任意長度的等差數列的陳述，這是對塞邁雷迪定理的一個修改。

而我們合作的方式是，本已經證明了長度為3的等差數列含有一個類似的結果。他表明，像素數這樣的集合包含大量長度為三的數列，甚至素數的某些子集也包含。但他的技術只適用于長度為三的數列，不適用于更長的數列。

但我有這些來自遍歷理論的技術，這是我當時一直在玩的技術，我比本更熟悉。所以如果我能證明某些與素數相關的集合的特定隨機性性質，就存在一定的技術條件擁有它。如果本能為我提供這個事實依據，我就可以得出定理。

但我要的是數論中一個非常困難的問題，他說我們不可能證明出來這個，所以他說，你能用一個弱假設來證明你的那部分定理嗎？他提出了一些他可以證明的東西，但對我來說太弱了，我不能用這個。所以類似的對話來回進行。

我們之間存在不同的作弊方式，我想作弊更多，他想作弊更少。但最終我們找到了一種屬性：A、他能證明；B、我可以使用，然后我們就可以證明我們的定理。所以要知道每次合作都會發生一些故事，沒有兩次完全相同。

Lean可以幫助科學家大規模地生產實驗結果

Q：如何看待Lean這一類編程語言？

陶哲軒：目前只有少數數學項目可以以這種方式劃分，在當前的技術水平下，大部分的Lean活動都是在形式化人類已經證明的定理，基本上一個數學論文就是一個定理或一種意義上的藍圖。

Lean可以將一個困難的陳述，比如一個大的定理，分解成100個小的引理，但通常不是所有的定理都寫得足夠詳細以至于每一個都可以直接分解。

而藍圖就像一份非常繁瑣的論文，其中每一步都盡可能詳細地解釋，并試圖使每一步都相對獨立，僅依賴于少數幾個已證明的前置陳述，因此藍圖中的每個節點都可以獨立處理，甚至不需要了解整個系統的運作方式。

嗯，這就像現代供應鏈，如果你想要制造一部 iPhone 或其他復雜物體，沒有人能夠獨立完成整個物體，但你可以讓一個專家，如果他們從其他公司獲得一些部件，就能將它們組合成稍大一些的部件。

Lex Fridman：我認為這是一個非常令人興奮的可能性，因為如果找到可以按這種方式分解的問題，就能擁有分布在全球各地的、成千上萬的貢獻者，是這樣么？

陶哲軒：對的。目前大多數數學都是理論性的，而實驗性數學則相對較少，我認為像Lean和其他軟件工具，比如GitHub之類的，將允許實驗數學以比我們現在所能做到的更大程度進行規模化。

現在如果你想要做任何關于數學模式或什么的數學探索，你只需要寫一些代碼來描述這個模式。我的意思是，有時候有一些計算機代數軟件包會提供幫助，但通常只是由一位數學家編寫大量的Python或其他代碼。畢竟編程是一項容易出錯的活，所以讓其他人協作編寫你的代碼模塊并不實際，因為如果其中一個模塊有bug，整個系統就不可靠。

這些定制的意大利面條式的代碼，由不是專業程序員而是由數學家編寫的，它們笨拙而且緩慢，所以很難大規模地生產實驗結果。但是有了Lean，數學家就能更好地進行這些工作。我有一個項目叫方程理論項目，在這個項目中我們生成了大約 2200 萬個抽象代數的小問題。

(圖片來源于方程理論項目頁)

抽象代數研究乘法和加法等運算以及抽象的性質，比如乘法的交換律，XY總是等于YX，至少對數學來說是這樣，這些運算遵循一些其它運算不遵循的法則。

但并非所有的法則都是通用的，任何操作都可能遵循其它操作不遵循的法則，所以我們生成了大約4,000種可能的代數法則，以適應不同的運算。

我們的問題是哪些法則會隱含哪些其他法則？嗯，例如，交換律是否隱含結合律？答案是否定，因為事實證明你可以描述一個操作，它遵守交換律但不遵守結合律，但另外一些法則確實蘊含其它法則，有時它們可以彼此替換，可以用一些代數進行證明。因此我們研究了這4000條法則之間的配對，大約有2200萬對組合，對于每一對我們都會問：這條法則是否蘊含了那條法則？如果是，請給出證明；如果不是，請給出反例。

這2200萬個問題，每一個問題都可以交給一個本科生代數學生，他們有相當大的機會能夠解決這些問題。盡管在這2200萬個問題中，有少數幾個，比如100個左右，確實非常難，但是很多問題都很簡單。這個項目的目標就是確定整個圖里哪些法則暗示了其它的法則。

Lex Fridman：這真是一個了不起的項目，一個好主意、好測試。這正是我們一直在討論的問題，規模令人矚目。

陶哲軒：是的，所以這種事情交給人工是不太可行的，我的意思是，最先進的技術在文獻中大約會有15 個方程以及它們的應用方式，這差不多就是人類研究論文所能達到的極限了。如果你需要將規模擴大，就需要把這個項目眾包，還需要信任——沒有人能檢查 2200 萬個這些證明。你需要實現自動化，這只有在有了Lean之后才成為可能。

我們也希望大量使用人工智能，所以這個項目已經接近完成了：在這2200萬個證明中，只剩下2個沒有得到解決。而實際上，關于這兩個，我們有兩份紙筆證明，今天早上我還在努力完成它。所以這個項目我們幾乎完成了。

Lex Fridman：這太厲害了，你能夠招募到多少人去完成這個項目？

陶哲軒：50個左右 ，這在數學上被認為是一個巨大的數字。所以我們有一篇有50位作者的論文，還有一個大的附錄說明每個人貢獻了什么。

Q：在這種多人參與的項目中，有沒有一種類似ELO評分的情況，可以根據貢獻者的專業水平來為他們的貢獻打分？

陶哲軒：這些精益項目的美妙之處在于，你可以自動獲取所有這些數據，你知道，所有內容都必須上傳到 GitHub，而 GitHub 會追蹤誰貢獻了什么。所以你可以在任何時間點生成統計數據，你可以說，哦，這個人貢獻了這么多行代碼或者其他什么的。但這些都是非常粗糙的指標，我不希望這會成為人們晉升評審的一部分。

不過我想在企業計算領域，人們已經在使用這些指標作為評估員工績效的一部分了，再次強調，這是一個有點可怕的方向，會導致學術水平下降，我們不喜歡指標。

Lex Fridman：但學術界卻在使用它們，只是使用的是舊指標，像論文數量。感覺這是一個有缺陷的指標，但也正朝著正確的方向發展，對嗎？

陶哲軒：是的，我認為研究它很有趣，我們可以做研究來判斷這些是否是更好的預測指標。有一個發現叫作古德哈特定律 (Goodhart’s law)，如果一個統計數據實際上被用來激勵表現，它就會變成一種游戲，而不再是一種有用的衡量標準。

因此，我們這個項目采用的是自我報告的形式。實際上，在科學領域存在關于人們貢獻類型的標準分類，有概念、驗證、資源提供、編程等等。

有一個包含12個左右類別的標準列表，嗯，我們要求每位貢獻者在一個包含所有類別所有作者的巨大矩陣中，在他們認為自己做出貢獻的地方打勾，并且給出一個粗略的想法。比如你可能做了一些編程工作、提供了一些計算資源，但沒有做任何紙筆驗證或其他工作什么的……

傳統上數學家們只是按姓氏的字母順序排列，而我們沒有這種傳統，科學也有第一作者、第二作者的劃分等等，我們也沒有。

我們為此感到驕傲，因為我們讓所有作者擁有平等的地位。

但它也不能完全上升到這個高度。十年前我參加了一個一些被稱為“多數學者項目”的事情，它是眾包數學，那時候還沒有Lean，所以它受限于需要一個主持人來檢查所有提交的貢獻是否真正有效，這實際上是一個巨大的瓶頸。嗯，我們仍然有一些項目有10位作者左右，但我們當時已經決定不要試圖劃分每個人做了什么，而是共同使用一個假名，因此我們以 Bwaki 的精神為基礎，創造了一個名為DHJ Polymath的虛構人物，Bwaki是20世紀一群著名數學家的筆名。

當時的論文是以DHJ Polymath這個筆名來發表的，所以我們都沒有獲得作者署名。實際上這不算一個好結果，原因有幾點，其中的一點是，如果你想要被考慮終身教職或者什么，你不能使用這篇論文作為你的出版物之一去提交，因為你沒有正式的作者署名。另一件事情是，直到很久以后人們才意識到，當人們提到這些項目時，只會提到項目中參與的最著名的人，而不是其他參與者。

所以這次我們嘗試了一些不同的：讓每個人都有作者身份，同時附上這個矩陣來解釋它如何運作。

Lex Fridman：僅僅是參與這樣的大型合作項目就足夠出色了。我看過幾年前Kevin Buzzard關于 Lean 編程語言的一個演講，你說這可能是數學的未來，這一點也很讓人興奮——世界最偉大的數學家之一也在擁抱這個似乎正在開創數學未來的東西。