# 陶哲軒：數學與物理中最難的問題，以及 AI 的未來 > 數學家陶哲軒談當下最棘手的數學與物理難題，以及 AI 會如何改變數學研究與證明的方式。 - 原標題：#472 – Terence Tao: Hardest Problems in Mathematics, Physics & the Future of AI - 期數：第 472 期 - 釋出日期：2025-06-14 - 嘉賓 / 主題：陶哲軒 - 網頁版：https://lex.qiaomu.ai/tw/ep/terence-tao/ - 官方頁面：https://lexfridman.com/terence-tao/ - 精讀字數：約 22467 字（閱讀約 50 分鐘） > 本文為 lex.qiaomu.ai 基於原始訪談的 AI 改寫中文精讀，非官方翻譯；引用請註明出處並連結網頁版。 2016年，陶哲軒發表了一篇論文，標題裡有四個字：有限時間爆破。他改造了納維-斯托克斯方程的一部分，讓它在一個虛構的物理規則下，把流體的所有能量在有限時間內逼進一個點。 這看起來像在搞破壞。他實際做的事情是排除一種可能性：如果有人想證明流體永遠不會爆破，有一條路已經被堵死了。 ## 一根針掉頭的謎題 1918年，日本數學家掛谷宗一提出了一個問題：一根無限細的針在平面上掉頭，最少需要多大面積？ 你可以在原地旋轉它，掃出一個圓，面積是四分之π。也可以像駕校教的三點掉頭那樣操作，面積縮小到八分之π。很長一段時間裡，人們以為這就是最優解。 然後貝西科維奇出現了。他證明，你可以用任意小的面積完成掉頭，0.01 也行，0.0001 也行。操作方式是一連串精巧的前後擺動，讓針掃過每一箇中間方向，佔用的總面積趨近於零。 二維的情況徹底搞清楚了。三維呢？ 陶哲軒打了個比方：假設哈勃望遠鏡是一根管子，你想讓它看到宇宙中每一顆星星，也就是指向每一個方向。空間當然是免費的，他假設空間極其寶貴，你想用最小的體積完成這件事。如果望遠鏡的厚度是零，答案和二維一樣，任意小都行。如果望遠鏡有一個很小的厚度 delta，最小的體積是多少？ 猜想是：體積下降得極慢，大致是對數級別。這個猜想經過大量工作後被證明了。 一個關於針頭掉頭的謎題，值得花幾十年去研究嗎？它和偏微分方程、數論、幾何、組合數學都有意想不到的聯絡。 水波可以一開始非常分散，然後在某個時刻聚焦到一個點。把時間反演，波紋會從四面八方匯聚，然後發生一次巨大的濺射，甚至可能產生奇點。幾何上發生了什麼？光沿著光線傳播，所有光子都在同一個點匯聚。如果掛谷猜想有一個否定的解答，就意味著可以非常高效地把指向不同方向的管子塞進一個極小的體積。對應的物理後果是：可以構造出大量在時空中的集中，波的振幅變得如此之大，以至於支配它們的方程不再是波動方程，變成了更復雜的非線性方程。 ## 一百萬美元的問題 納維-斯托克斯方程描述了水和空氣這樣的流體的運動。克雷數學研究所把它列為七個千禧年大獎難題之一，解出一個給一百萬美元。七個問題裡，目前只有一個被解決，龐加萊猜想。 納維-斯托克斯的核心問題是：如果你從一個光滑的水流速度場出發，它會不會在某個點變得無限大？也就是產生奇點。 現實中我們沒見過這種事。你在浴缸裡拍水，水不會爆炸，也不會以光速飛出去。數學上，它是否可能？ 陶哲軒說，這正是數學家和絕大多數人的區別。如果一件事在 99.99% 的情況下成立，對大多數領域來說就夠了。數學家關心的是，是不是 100% 的所有情況都被覆蓋了。 為什麼證明這件事這麼難？陶哲軒的短回答是：麥克斯韋妖。 盒子裡有兩種氣體，氧氣和氮氣，一開始氧在一邊，氮在另一邊，中間沒有隔板。它們會混合，然後保持混合。沒有理由讓它們重新分開。原則上，因為分子之間的大量碰撞，可能存在某種詭異的共謀，一個微觀的麥克斯韋妖，每次氧和氮碰撞時都讓它們以特定的方式彈開，讓氧慢慢漂到一邊，氮漂到另一邊。這種配置出現的機率極低，低到我們永遠看不到，數學上它是可能的，而我們無法排除它。 這個現象在數學裡到處都是。π 的數字看起來沒有規律，我們相信它們沒有規律，長期來看 1 和 2 出現的頻率應該差不多。也許 π 的數字裡藏著一個妖，每次你計算更多位數，它就讓某個數字偏多一點。這種共謀不應該發生，沒有理由發生，以我們目前的技術，無法證明它不發生。 回到流體。流體有能量，因為流體在運動，能量會被輸運到各處。水有黏性，如果能量分散在很多位置，黏性會把它耗散掉，能量歸零。這是我們實際觀察到的：你攪動水，產生湍流和波浪，最終它會平靜下來，速度越小越平靜。 也許存在某種妖，不斷把能量推向越來越小的尺度，讓流體運動得越來越快。速度越快，黏性的相對效果越弱。於是可能出現一種自相似團塊的情景：能量從大尺度轉移到一個小區域，然後以更快的速度轉移到更小的區域，每次耗時大約是上一次的一半。這樣下去，所有能量會在有限時間內集中到一個點。 有限時間爆破。 現實中不會發生，因為水是湍流的。一個大渦旋會分裂成小渦旋，它會把能量傳給三四個小渦旋，然後它們再各自分裂。能量被分散到黏性足以控制一切的程度。如果能量能被某種方式集中起來，保持在一起，而且速度足夠快，讓黏性來不及平息它，爆破就可能發生。 > 如果有 10 件事讓你的生活變得困難，找一個版本的問題，關掉其中 9 件，只留 1 件，然後解決它。（陶哲軒） ## 數學家可以修改物理定律 過去有很多人嘗試證明納維-斯托克斯方程的全域性正則性，也就是速度永遠保持光滑，不會爆破。全都失敗了。總有一些符號錯誤或細微的疏漏，無法補救。 陶哲軒想做的事情不一樣。他想解釋為什麼我們無法否證有限時間爆破。 真實的流體方程太複雜，他做不到。如果能把方程平均化，關掉某些水相互作用的方式，只保留他想要的那些。比如流體可以把能量從大渦旋傳給這個小渦旋或那個小渦旋，他關掉通往其中一個的通道，只讓能量流向另一個，同時保持能量守恆。 他工程化地製造了一個爆破，方式是改變物理規則。這是數學家被允許做的事情之一：修改方程。 這怎麼幫助證明？它提供了一個障礙。通常關掉某些相互作用會讓方程變得不那麼非線性，更規則，更不容易爆破。他發現，透過關掉一組精心設計的相互作用，他可以強迫所有能量在有限時間內爆破。這意味著，如果你想證明真實納維-斯托克斯方程的正則性，你必須用到真實方程中他的虛構方程不具備的某個特徵。這就排除了一整類方法。 數學不只是拿起一個能用的技術去用，還要不去用那些不能用的技術。對於真正困難的問題，你可能會想到幾十種方法似乎都適用，只有積累了大量經驗之後，你才意識到這些方法根本行不通。有了這些反例，你就不用浪費精力在那些已經被證明不可能成功的事情上。 這裡的關鍵概念是超臨界性。偏微分方程常常是不同力量之間的拔河。納維-斯托克斯裡，耗散力來自黏性，線性，讓一切平靜下來。如果只有黏性，什麼壞事都不會發生。還有輸運項，能量可以從一個位置被流體運動帶到另一個位置，這是非線性效應，也是所有麻煩的來源。 如果耗散項佔主導，你得到正則性。如果輸運項佔主導，我們不知道會發生什麼。湍流，不可預測。 有時候這兩種力在小尺度上平衡，在大尺度上不平衡，或者反過來。納維-斯托克斯是超臨界的：尺度越小，輸運項比黏性項強得多。這就是問題困難的原因。二維情況下，蘇聯數學家拉德任斯卡婭在 60 年代證明了不會爆破。二維的納維-斯托克斯是臨界的，輸運和黏性的效果即使在極小的尺度上也大致相同。我們有大量技術處理臨界和次臨界的方程，證明正則性。超臨界方程，情況不清楚。 陶哲軒做了大量工作，後續也有很多研究，表明對於許多其他型別的超臨界方程，你可以構造各種爆破的例子。一旦非線性效應在小尺度上壓倒線性效應，各種壞事都可能發生。 這也解釋了為什麼我們能預測行星運動幾百萬年，卻無法預測兩週後的天氣。行星運動容易處理，你可以把行星近似成質點，整體行為才重要。天氣是超臨界方程，在極細的尺度上有大量奇怪的事情發生。你不能只說洛杉磯的溫度是這個，風速是那個，你必須知道每一個微小尺度的資訊。 ## 用水造一臺圖靈機 陶哲軒有一個更瘋狂的想法：構造一臺液體計算機，然後用停機問題來證明流體動力學的某些結論。 這個想法來自他構造平均方程爆破的工作。最樸素的做法是每次能量到達一個尺度就立刻把它推到下一個尺度。這在五維及以上行得通。在三維，出現了一個奇怪的現象：如果你總是試圖把能量推到越來越小的尺度，能量會同時分散到許多尺度上，每一層都留下一些能量。這反而讓黏性有機可乘，把一切耗散掉。直接爆破在三維不成立。 他需要的是一個延遲機制，像氣閘一樣。能量在一個尺度上運作，被推到下一個尺度，在那裡等著，直到大尺度的能量全部轉移過來。然後才開啟下一道閘門，繼續推。這樣能量一次只集中在一個尺度上，不會被分散，就能抵抗黏性。 為了做到這一點，他構造了一個相當複雜的非線性項。它的構造方式像電子電路。他感謝他的妻子，她是電氣工程師，跟他講過設計電路的事情。如果你想要一個電路做某件事，比如讓一個燈閃爍，你可以用更基本的元件，電容、電阻，搭出來，畫一張圖，然後順著圖就能看出電流會在這裡積累，然後停止，然後做下一件事。 他知道怎麼構造電阻和電容的數學類比，然後把它們堆疊起來，創造出能開啟一道閘門的東西。有一個時鐘，當時鍾到達某個閾值，閘門關閉。這變成了一個魯布·戈德堡式的機器，用數學描述。這個辦法最終成功了。 他意識到，如果同樣的構造對真實的流體方程也成立，如果水的方程支援計算，那麼你可以想象一種蒸汽朋克，不，應該是水朋克的東西。現代計算機是電子的，由電子透過極細的導線，與其他電子相互作用。你可以想象，用具有一定速度的水脈衝代替電子。也許有兩種配置對應於位元的 0 和 1。如果兩個運動的水體碰撞，它們會以某種新的配置出來，就像與門或或門，輸出以非常可預測的方式依賴於輸入。你可以把這些串聯起來，也許創造一臺圖靈機。然後你就有了完全由水構成的計算機。 如果有了計算機，也許你可以做機器人，液壓之類的東西。你可以創造一臺機器，本質上是流體版的馮·諾依曼機。 馮·諾依曼提出，如果你想殖民火星，把人和機器運過去的成本高得離譜。如果你能運送一臺機器到火星，這臺機器能夠採礦，製造材料，冶煉，然後建造更多自己的複製品，你就能逐漸殖民整個星球。 如果你能造一臺流體機器，一個流體機器人。它的使命是創造一個更小的自己，處於某種冷狀態，還沒啟動。一旦準備好，大的水機器人配置會把所有能量轉移給小的配置，然後關機。然後它清理自己，留下的是最新的狀態，它會啟動，做同樣的事情，更小更快。方程有一種縮放對稱性，一旦你做到這一點，它就能不斷迭代。原則上，這會對真實的納維-斯托克斯方程造成爆破。 這就是他為平均納維-斯托克斯所完成的事情。它提供了一張解決這個問題的路線圖。當然，這是白日夢，因為要實現它，缺失的東西太多了。他造不出這些基本的邏輯閘，沒有這些特殊的水配置。有一些候選者，包括渦環，可能行得通。模擬計算比數字計算麻煩得多，總是有誤差，你需要大量的糾錯。他也不知道怎麼完全關閉大機器，讓它不干擾小機器的寫入。原則上，一切都可以發生，不違反任何物理定律，所以這是這件事可能的證據。 還有其他團隊在嘗試讓納維-斯托克斯爆破，他們的方案遠沒有這麼複雜。他們在追求更接近直接自相似模型的方法，雖然原樣行不通，可能有更簡單的方案。 數學很擅長髮現看似完全不同的問題之間的聯絡，只要數學形式相同，就能建立聯絡。元胞自動機就是先例。最著名的是康威的生命遊戲。一個無限離散網格，每個格子要麼有細胞要麼空。規則很簡單，決定細胞如何演化。有時候細胞活著，有時候死掉。陶哲軒當學生的時候，螢幕保護程式經常跑這個，看起來非常混沌，有時候像湍流。後來人們在這個遊戲裡發現了越來越有趣的結構。 比如滑翔機。一個很小的配置，四五個細胞，會演化並沿某個方向移動。這就像渦環。 生命遊戲是一個離散方程，納維-斯托克斯是連續方程，數學上有相似的特徵。隨著時間推移，人們在生命遊戲裡發現了越來越多有趣的東西。它只有三四條規則，你可以設計各種有趣的配置。有一種叫滑翔機槍，什麼都不做，只是一個個吐出滑翔機。經過大量努力，人們造出了滑翔機的與門和或門。一個巨大的、看起來很荒謬的結構，如果這裡有滑翔機流進來，那裡也有，可能會產生輸出的滑翔機。如果兩股都有，就有輸出，如果只有一股，就什麼都沒有。一旦你能造出這些基本門，從軟體工程的角度，你幾乎可以造任何東西。你可以造圖靈機，巨大的蒸汽朋克式的裝置，看起來很可笑。人們還造出了生命遊戲裡的自複製物體，一臺巨大的機器，經過漫長的時間，裡面看起來像滑翔機槍在做這些非常蒸汽朋克的計算，它會創造出另一個自己，可以複製。 這些工作很多是業餘數學家眾包完成的。陶哲軒知道這些工作，這是啟發他把同樣的事情搬到納維-斯托克斯的部分原因。模擬比數字差得多，你不能直接把生命遊戲裡的構造搬過來，它表明這是可能的。 這種湧現現象很有意思。區域性規則在規模上創造出極其複雜的動態結構。陶哲軒指出，你只能在精心準備的初始條件下得到這些湧現的複雜結構。那些滑翔機槍、門、自走機器，如果你隨便扔一些細胞上去，什麼都不會看到。這和納維-斯托克斯的情況類似：在典型的初始條件下，不會有任何奇怪的計算發生。透過工程，透過精心設計，你可以做出聰明的構造。 能不能證明只有透過工程才能創造有趣的東西？這是數學裡反覆出現的挑戰，陶哲軒稱之為結構與隨機性的二分。數學中能生成的大多數物件是隨機的，看起來隨機。只有很小一部分有模式。證明某個東西有模式，你可以直接構造。如果某個東西有簡單的模式，你能證明它每隔一段時間重複，你就證明了。比如你可以證明大多數數字序列沒有模式。如果我們給你一個特定的模式，比如 π 的數字，你怎麼證明它沒有某種奇怪的模式？ 陶哲軒花了大量時間證明所謂的結構定理或逆定理，給出測試某個東西是否非常有結構的方法。有些函式是加性的。如果 A 加 B 乘以 10 等於 A 乘以 10 加 B 乘以 10，這就是加性的。有些函式幾乎加性但不完全加性。比如乘以根號 2 再取整數部分，10 乘以根號 2 大約是 14 點幾，所以 10 對映到 14，20 對映到 28。這種情況下加性成立。因為取整，有時會有舍入誤差，A 加 A 的結果不完全等於兩個單獨輸出的和，是和加減一。它幾乎是加性的，不完全。 數學裡有很多有用的結果，如果函式表現出某種結構，那背後一定有原因。原因是存在另一個附近的函式，完全有結構，解釋了這種部分模式。有了這些逆定理，就創造了一種二分：你研究的物件要麼完全沒有結構，要麼與某種有結構的東西相關。無論哪種情況，你都能取得進展。 ## 無限猴子與有限化 塞邁雷迪定理是這種二分的好例子。1970 年代證明，任何足夠大的、具有正密度的數集都包含任意長度的等差數列。 比如奇數密度是二分之一，包含任意長度的等差數列。這很明顯，因為奇數非常有結構。塞邁雷迪定理也適用於隨機集合。如果隨機保留一半的數，這個集合沒有任何模式，僅僅因為隨機漲落，你仍然會得到大量等差數列。 這就是無限猴子定理。如果有無限多隻猴子在房間裡打字，幾乎必然，其中一隻會生成《哈姆雷特》的完整劇本，或者任何有限長度的文字。只是需要很長時間，非常長的時間。 無限吸收了很多罪惡。 人類怎麼理解無限？你可以把無限看作一個沒有上界的有限數的抽象。現實中沒有任何東西是真正無限的，你可以問，如果我有任意多的錢會怎樣，如果我能任意快會怎樣。數學家把這種理想化形式化了，與其說某個東西非常大或非常小，說它恰好是無限或零。數學在這樣做的時候往往變得更乾淨。物理學裡有個笑話，假設奶牛是球形的。現實世界的問題有各種現實世界的效應，你可以理想化，把某些東西送到無限，某些送到零，數學變得簡單得多。 無限也有陷阱。有限個項相加，交換順序沒問題。無限個項，你可以玩把戲，一個級數收斂到一個值，重新排列後突然收斂到另一個值。你必須知道自己在做什麼。需要引入 epsilon 和 delta，有一套嚴謹的推理方式幫你避免錯誤。 近年來，人們開始把無限極限下成立的結果有限化。你知道某件事最終會成立，不知道什麼時候。現在給我一個速率。如果是一大群有限的猴子，要等多久才能看到《哈姆雷特》？這個問題更定量，可以用純有限的方法攻擊，用有限的直覺。結果是指數級的，取決於你要生成的文字長度。這就是為什麼你永遠看不到猴子創作《哈姆雷特》。你也許能看到它們創作一個四個字母的單詞，再大就不行了。 陶哲軒個人覺得，一旦把無限陳述有限化，它就變得直覺多了，不再那麼奇怪。缺點是有限化的版本混亂得多。無限版本通常先被發現，幾十年後人們才把它有限化。 ## 數學、物理、工程：三種看世界的方式 科學總體上涉及三樣東西的互動：真實世界，我們對真實世界的觀察，我們關於世界如何運作的心智模型。 我們無法直接接觸現實。我們只有觀察，觀察是不完整的，有誤差。很多情況下我們想知道明天的天氣，我們還沒有那個觀察，我們想要一個預測。 我們有簡化模型，有時做出不切實際的假設，球形奶牛之類的東西。這些是數學模型。 數學關心模型。科學收集觀察，提出可能解釋這些觀察的模型。數學留在模型裡，問這個模型的後果是什麼，會做出什麼預測，是否符合觀察資料。 數學在其他學科中不尋常的地方在於，我們從假設出發，從模型的公理出發，問什麼結論能從中得出。幾乎所有其他學科，你從結論出發。我想做這個，我想建一座橋，我想賺錢，然後找通往那裡的路徑。很少有，假設我這樣做了會怎樣這種推測。規劃和建模。推想小說也許是另一個地方，基本就這樣了。我們生活中做的大多數事情都是結論驅動的，包括物理學和科學。他們想知道小行星會去哪裡，明天的天氣是什麼。數學還有這個從公理出發的方向。 理論更強大還是實驗更強大？你需要兩者，自上而下和自下而上。隨著時間推移，觀察、理論和建模都應該越來越接近現實。一開始它們總是相距很遠，你需要一個來找出往哪裡推另一個。如果你的模型預測了實驗沒有預測到的異常，那告訴實驗者去哪裡找更多資料來改進模型。來來回回。 數學內部也有理論和實驗的分量。直到最近，理論幾乎完全主導。99% 的數學是理論數學，只有極少的實驗數學。人們確實做，如果想研究素數，可以生成大資料集。有了計算機之後，我們做得多了一點。更早以前，比如高斯，他發現素數定理這個數論中最基本的定理，預測一百萬以內、一萬億以內有多少素數。他做的事情是計算，大部分自己算，也僱了人類計算員，職業做算術的人，計算前十萬個素數，做表格，做預測。這是實驗數學的早期例子。 直到最近，理論數學成功得多。複雜的數學計算在最近之前根本不可行。即使現在有強大的計算機，只有一些數學東西能數值探索。 有一個東西叫組合爆炸。如果你想研究塞邁雷迪定理，研究 1 到 1000 的所有子集。只有 1000 個數，能有多難？結果是 1 到 1000 的子集數量是 2 的 1000 次方，比任何計算機能列舉的都大得多。有些數學問題很快變得無法用暴力計算直接攻擊。國際象棋也是著名例子。棋局的數量，我們無法讓計算機完全探索。現在有了 AI，有了工具來探索這個空間，沒有 100% 保證成功，透過實驗。我們現在可以經驗性地解決國際象棋。有非常好的 AI，不探索博弈樹中的每一個位置，找到了很好的近似。人們正在用這些象棋引擎做實驗象棋。他們重新審視舊的象棋理論，這種開局是好棋，那種不是，用引擎來改進，有時推翻傳統智慧。陶哲軒希望數學未來也會有更大的實驗成分，也許由 AI 驅動。 在國際象棋的情況裡，AI 並沒有提供形式化的解釋。它只是說哪個位置更好，人類可以從中直覺，然後構建理論。陶哲軒提到柏拉圖洞穴寓言。人們觀察現實的影子，相信他們觀察到的就是現實。數學家和所有人類都在看影子嗎？我們能否真正接觸現實？ 這三樣東西，真實現實、觀察、模型，技術上是不同的，陶哲軒認為它們永遠會不同，可以越來越近。接近的過程常常意味著你必須拋棄最初的直覺。天文學提供了好例子。最初的世界模型是平的，因為它看起來平，很大，而宇宙的其他部分，天空，不是。太陽看起來很小。你從一個離現實很遠的模型開始，它符合你現有的觀察，看起來不錯。隨著你做出越來越多的觀察，模型被拖著一起走。我們不得不認識到地球是圓的，會自轉，繞太陽轉，太陽系繞銀河系轉，宇宙在膨脹，膨脹在加速，今年還有證據表明加速本身不是恆定的。 我們有一個模型很好地擬合資料，只需要指定幾個引數。人們說那是湊數因子，有足夠多的湊數因子你可以解釋任何事。數學上，你希望模型引數少，觀察資料點多。如果你的模型有 10 個引數解釋 10 個觀察，那是完全沒用的模型，叫過擬合。如果模型有兩個引數解釋一萬億個觀察，這基本上就是暗物質模型，它有 14 個引數，解釋天文學家 petabytes 的資料。 物理數學理論可以看作宇宙的壓縮，資料壓縮。你有 petabytes 的觀察，想壓縮成一個五頁紙能描述的模型，指定一定數量的引數。如果它能以合理的精度擬合幾乎所有觀察，壓縮得越多，理論越好。 宇宙可壓縮這件事本身就是巨大的驚喜。愛因斯坦說過，宇宙最不可理解的事情是它是可以理解的。不只是可理解，你還能寫出 E 等於 MC 平方這樣的方程。 這有可能的解釋。數學裡有個現象叫普適性。許多複雜系統在宏觀尺度上的行為來自大量微觀尺度的微小相互作用。通常因為組合爆炸，你會認為宏觀尺度的方程必須比微觀尺度的方程複雜無限倍、指數倍。如果你想完全精確地解它們，確實如此。某些規律在宏觀尺度湧現，幾乎不依賴於微觀尺度發生了什麼，或者只依賴於很少的引數。想模擬盒子裡 quintillion 個粒子的氣體，你只需要知道溫度和壓強和體積，五六個引數，就能模擬幾乎一切。我們對普適性的數學理解遠不如我們希望的那樣，有些簡單得多的玩具模型，我們很好地理解為什麼普適性會發生。最基本的是中心極限定理，解釋了為什麼鐘形曲線在自然界到處都是，為什麼那麼多東西服從高斯分佈。 有時候不是。如果許多輸入都以某種系統性方式相關，你會得到遠離鐘形曲線的東西。知道中心極限定理什麼時候失敗也很重要。2008 年全球金融危機是著名例子。人們以為抵押貸款違約有高斯型行為，如果一切都去相關，十萬美國人的違約比例會是一個漂亮的鐘形曲線，你可以管理期權和衍生品的風險，有很美的理論。如果經濟中有系統性衝擊，能推動所有人同時違約，那就是非常非高斯的行為，這在 2008 年沒有被完全考慮進去。現在人們對系統性風險是更大的問題有了更多認識，模型漂亮不代表符合現實。 ## 刺蝟與狐狸 陶哲軒以橫跨數學眾多領域的廣度著稱。菲爾茲獎得主蒂姆·高爾斯說他是最接近希爾伯特的人。 數學中有連線所有不同領域的線索嗎？有深層結構嗎？ 確實有很多連線的線索。數學的很多進步可以表示為把兩個之前沒有聯絡的領域連線起來。一個古老的例子是幾何和數論。古希臘時代，它們被認為是不同的學科。歐幾里得兩者都做，人們不覺得它們相關。直到笛卡爾發展了解析幾何，你可以用兩個實數引數化平面這個幾何物件。幾何問題變成了關於數字的問題。今天這感覺幾乎是平凡的，平面就是 x 和 y，因為我們就是這樣被教的，已經內化了。這個進展很重要，兩個領域被統一了。這個過程在數學中一遍又一遍地發生。代數和幾何曾經分開，現在我們有代數幾何連線它們。 數學家有不同風格。刺蝟和狐狸。狐狸知道很多事情，每樣知道一點。刺蝟知道一件事，知道得非常透徹。數學裡兩者都有，也有人能扮演兩種角色。理想的合作需要多樣性，一個狐狸和很多刺蝟合作，或者反過來。陶哲軒認為自己主要是狐狸。他喜歡套利，學習一個領域怎麼運作，學會那個領域的技巧，然後去另一個人們認為不相關的領域，但我能改造這些技巧。 有些數學家比他深得多，是真正的刺蝟。他們知道一個領域的一切，在那個領域裡快得多、有效得多。他能給他們額外的工具。 陶哲軒更適應狐狸正規化。他喜歡找類比、敘事。如果他在一個領域看到一個結果，喜歡這個結果，不喜歡證明，用了他不熟悉的數學，他常常嘗試用自己喜歡的工具重新證明它。通常他的證明更差，透過這個練習，他能看到原來的證明想做什麼，從而理解那個領域的工具。非常探索性，在瘋狂領域做瘋狂的事情，經常重新發明輪子。刺蝟風格更學術，知識驅動。你跟上一個領域的所有發展，知道所有歷史，很好地理解每種技術的強項和弱點。更多依賴計算，而不是找敘事。他也能做，其他人非常擅長。 陶哲軒年輕時，數學更像解謎活動。什麼時候第一次遇到一個問題或證明，意識到數學有優雅和美感？ 他到普林斯頓讀研究生時，約翰·康威在那裡。他記得最早參加的研究講座之一是康威講他所謂的極端證明。康威有驚人的方式思考各種事情，你不會正常想到的方式。他把證明本身看作佔據某個空間。如果你想證明某件事，比如有無窮多個素數，你有不同的證明，可以按不同軸排序。有些證明優雅，有些長，有些初等。所有證明的空間本身有某種形狀，他感興趣的是這個形狀的極端點。所有證明中，最短的那個，犧牲其他一切，或者最初等的，或者別的。 他舉了一些著名定理的例子，給出他認為在各自特性上的極端證明。陶哲軒覺得這非常開眼界。不只是得到一個證明有趣，有了證明之後，嘗試在各種特性上最佳化它，證明本身有工藝性。 這影響了他的寫作風格。本科時做作業，你被鼓勵寫下任何能用的證明交上去，只要打勾就行。如果想讓你的結果有影響力，被讀者閱讀，它不能只是正確。它還應該讀起來愉快，有動機，能適應推廣到其他東西。很多其他學科也一樣，比如程式設計。數學和程式設計有很多類比。你可以寫能完成任務的義大利麵條式程式碼，快速粗糙，能用。有好的原則寫出好的程式碼，讓別人能用，能在此基礎上構建，bug 更少。數學也類似。 程式設計裡有個活動叫程式碼高爾夫，用不同程式語言寫出最短的程式完成特定任務。有比賽。這是壓力測試程式，或者在這種情況下，證明，以及不同語言的好方法。也許用不同的記號完成不同的任務。這看起來像無聊的練習，它能產生各種洞見，如果你沒有這個人為的目標去追求，你可能看不到。 什麼是最美或最優雅的方程？人們常看簡單性。E 等於 MC 平方。幾個概念走到一起，這就是為什麼尤拉恆等式常被認為是最美的數學方程。陶哲軒覺得最有吸引力的是不同事物之間的聯絡。尤拉恆等式用了所有基本常數。這很可愛，對他來說，指數函式，尤拉發明來度量指數增長，複利或衰減，任何連續增長、連續減少的東西，增長和衰減，或膨脹和收縮，都由指數函式建模。π 來自圓和旋轉。你想把一根針旋轉一百度，需要旋轉 π 弧度。i，複數，代表交換虛軸的 90 度旋轉，方向的變化。指數函式代表沿你已經在的方向的增長和衰減。當你在指數里放一個 i，運動不再是你當前位置的方向，垂直於你當前位置的方向，也就是旋轉。E 的 πi 次方等於負一告訴你，如果你旋轉 π 的時間，你最終到達相反的方向。它透過膨脹和指數增長統一了幾何，透過復化、旋轉 πi 這個行為統一了動力學。它連線了動力學、幾何和複數。它們在數學中曾經是鄰居，因為這個恆等式。 記號碰撞是有價值的。這是確認你有了正確的概念。當你第一次學任何東西，你必須度量它們，給它們命名。一開始因為你的模型離現實太遠，你把最好的名字給了錯誤的東西，後來才發現什麼是真正重要的。 物理學家有時會這樣做，結果還好。E 等於 MC 平方，其中一個大東西是 E。亞里士多德最初提出運動定律，然後伽利略、牛頓，他們看到能度量的東西，質量、加速度、力，牛頓力學，F 等於 ma，是著名的牛頓第二定律。那些是主要物件。他們在理論中給了它們核心地位。只有後來人們開始分析這些方程，發現似乎總有守恆量。特別是動量和能量。物體有能量不是顯而易見的。它不像質量和速度那樣能直接度量。隨時間推移，人們意識到這實際上是一個非常基本的概念。 哈密頓在 19 世紀最終把牛頓物理定律重新表述為哈密頓力學，能量，現在叫哈密頓量，成為主導物件。一旦你知道如何度量任何系統的哈密頓量，你就能完全描述動力學，所有狀態會發生什麼。它真的是一箇中心角色，最初並不明顯。這種視角變化在量子力學出現時非常有幫助。早期研究量子力學的物理學家很難適應他們的牛頓式思維，一切都是粒子，到了量子力學，一切都是波，看起來非常奇怪。你問 F 等於 ma 的量子版本是什麼，很難回答。結果是，在經典力學中如此秘密地在幕後運作的哈密頓量，也是量子力學的關鍵物件。也有一個叫哈密頓量的物件。它是不同型別的物件，是算符而不是函式，同樣，一旦你指定它，你就指定了整個動力學。 薛定諤方程告訴你量子系統一旦有了哈密頓量如何演化。並排看，它們看起來完全不同。一個涉及粒子，一個涉及波。有了這個中心性，你可以開始把很多直覺和事實從經典力學轉移到量子力學。比如諾特定理。物理系統裡每個對稱性都有守恆律。物理定律是平移不變的，我向左移動十步，經歷同樣的物理定律，對應動量守恆。我轉某個角度，還是同樣的物理定律，對應角動量守恆。我等十分鐘，還是同樣的物理定律，時間平移不變，對應能量守恆。對稱性和守恆之間有根本聯絡。量子力學裡也是，即使方程完全不同。因為它們都來自哈密頓量，哈密頓量控制一切，每當哈密頓量有對稱性，方程就有守恆律。有了正確的語言，事情變得乾淨多了。 我們無法統一量子力學和廣義相對論的一個問題是，我們還沒搞清楚基本物件是什麼。我們必須放棄時空是近乎歐幾里得空間的概念，我們知道在極小尺度會有量子漲落，有時空泡沫。試圖用笛卡爾座標 x、y、z 是行不通的。我們不知道用什麼替代。我們沒有那些概念，沒有那個類似哈密頓量的東西來組織一切。 直覺認為存在大統一理論嗎？陶哲軒相信存在。物理學歷史就是統一的歷史，很像數學。磁和電曾經是分開的理論，麥克斯韋統一了它們。牛頓統一了天體的運動和地球上物體的運動。這應該會發生。問題在於，物理學是自己成功的受害者。我們兩個大理論，廣義相對論和量子力學，現在太好了，它們一起覆蓋了我們能做的一切觀察的 99.9%。你必須去極端的粒子加速器，或者早期宇宙，或者非常難測量的東西，才能得到偏離這兩個理論的結果，才能搞清楚如何把它們結合起來。他有信心，我們已經做了幾個世紀，之前取得過進展，沒有理由停止。 陶哲軒會發展出大統一理論嗎？經常發生的是，物理學家需要某種數學理論時，數學家往往之前已經研究出了某種前身。愛因斯坦意識到空間是彎曲的，去找數學家，問有沒有關於彎曲空間的理論。數學家說，黎曼研究過。黎曼發展了黎曼幾何，正是關於各種一般彎曲空間的理論，幾乎正是愛因斯坦理論所需要的。這又回到了數學的不合理有效性。解釋宇宙的好的理論，往往也涉及那些很好地解決數學問題的數學物件。最終它們都只是用有用的方式組織資料。 弦理論是幾十年的領先候選，陶哲軒覺得它正在慢慢失寵，因為不符合實驗。實驗很難，因為兩個理論都太有效。另一個問題是，你不只是偏離時空，你進入瘋狂數量的維度，做各種奇怪的事情，我們已經離最初平坦地球的直覺太遠了，很難用我們有限的猿類後代認知去直覺那個現實到底是什麼。 這就是類比為什麼重要。圓的地球不直覺，因為我們被困在上面。圓的東西總體上我們有很好的直覺，我們對光如何運作有興趣。用圓的地球、圓的月亮和模型來搞清楚日食月食和太陽月亮的相位是很好的練習。你可以拿一個籃球、一個高爾夫球和一個光源，自己做這些事。直覺在那裡，你必須轉移它。 現代科學是自己成功的受害者。為了更精確，它必須越來越遠離你最初的直覺。對沒有經歷過整個科學教育過程的人來說，它看起來更可疑。我們需要更多接地氣的東西。有些科學家做很好的科普，很多科學東西你可以在家做。陶哲軒最近和格蘭特·桑德森做了個影片，講古希臘人如何測量月球距離、地球距離，用的技術你也可以自己複製。不一定要花哨的太空望遠鏡和嚇人的數學。 視角轉換很重要。旅行開闊心靈，這是智力旅行。把自己放在古希臘人的心智中，或者其他時代的人，提出假設，球形奶牛，隨便什麼，推測。這是數學家做的，也是藝術家做的。 考慮到極端約束，你仍然能說非常有力的事情。這是鼓舞人心的地方。回顧歷史，當你沒有很多工具來搞清楚事情時，能搞清楚多少東西。 ## 閉著眼睛在地上打滾 陶哲軒研究過波對映方程，也叫 sigma 場模型。它描述的是可能存在於時空之上的某些場的方程，與時空引力本身無關。愛因斯坦方程描述時空本身，還有其他場存在於其上。電磁場，楊-米爾斯場。有一整個層級的不同方程，愛因斯坦被認為是最非線性、最困難的之一，相對低的是波對映方程。一個波，在每一點固定在球面上。你可以想象空間中一堆箭頭，指向不同方向，它們像波一樣傳播。如果你擺動一個箭頭，它會傳播，讓所有箭頭移動，像麥田裡的麥浪。 陶哲軒感興趣的是全域性正則性問題。能量可能在某一點聚集嗎？他考慮的方程是臨界的，在所有尺度上行為大致相同。他勉強能證明你不能強迫所有能量集中到一個點，能量必須稍微分散一點，然後保持正則。這是 2000 年的事。這也是他後來對掛谷問題感興趣的部分原因。 這個問題非常非線性，因為球面的曲率。有某些非線性效應是非微擾效應。正常看它比波動方程的線性效應大。即使能量很小，也很難控制。 他發展了一種規範變換。方程有點像麥浪的演化，都在來回彎曲，有很多運動。如果你想象在不同點安裝小相機，試圖以捕捉大部分運動的方式移動，在這個穩定化的流下，流變得更線性。他發現了一種變換方程的方式來減少非線性效應，然後能解方程。他是在訪問澳大利亞的姑姑時找到這個變換的。他試圖理解所有這些場的動力學，不能用紙筆，也沒有足夠的計算機設施做模擬。他最後閉著眼睛，躺在地板上，想象自己是這個向量場，滾來滾去，試圖看到如何改變座標，讓所有方向上的東西以合理線性的方式行為。他姑姑走進來看到他在這樣做，問他在幹什麼。答案很複雜。好吧，你是個年輕人，我不問。 陶哲軒怎麼處理困難問題？大量紙筆。作為數學家你學會的一件事，他稱之為戰略性地作弊。數學的美妙之處在於你可以改變問題，改變規則，隨心所欲。其他領域不允許。如果你是工程師，有人說在這條河上建一座橋，你不能說我想在這裡建，或者我想用紙而不是鋼。數學家，你想做什麼都行。像玩一個有無限作弊碼的電腦遊戲。有個維度很大，我把它設為一，先解決一維問題。有個主項和一個誤差項，我做球形奶牛假設，誤差項是零。 你應該這樣解決問題，不是在鋼鐵俠模式裡讓事情最大化地困難。任何合理的數學問題，如果有 10 件事讓你的生活困難，找一個版本的問題，關掉其中九個，只留一個，解決它。然後解九次作弊，解十次作弊遊戲就平凡了，解九次。你解決一個問題，教你如何處理那個特定的困難。然後關掉那個，開啟另一個，解決那個。等你知道如何分別解決 10 個困難，然後開始幾個幾個地合併。 他小時候看很多香港動作片。每次打鬥場景，主角被一百個壞人包圍，編排總是讓他一次只打一個人，打敗那個，再下一個。因此他能打敗所有人。如果他們更聰明一點，一起湧上來，電影會難看多了，他們能贏。 他主要用紙筆。辦公室有四塊大黑板，有時他必須把關於問題知道的一切寫在四塊黑板上，然後坐在沙發上，看整個東西。很多繪圖，很多隻有他自己能看懂的塗鴉。黑板的美妙在於可以擦，非常有機。他開始更多地用電腦，部分因為 AI 讓簡單的編碼事情容易多了。以前想畫一箇中等複雜的函式，有迭代什麼的，他得記得怎麼設定 Python 程式，for 迴圈怎麼工作，除錯，要花兩個小時。現在 10 到 15 分鐘就行。他用越來越多電腦做簡單探索。 ## Lean：一個極度挑剔的同事 Lean 是一種計算機語言，像 Python 和 C 這樣的標準語言，大多數語言的重點是可執行程式碼。程式碼行做事情，翻轉位元，讓機器人移動，在網際網路上傳遞文字。Lean 也可以做這些，能作為傳統語言執行，它還能產生證書。Python 這樣的語言可能做計算，給你答案是七。3 加 4 等於 7 嗎？Lean 不僅產生答案，還產生如何得到答案的證明，3 加 4 和所有步驟。它建立更復雜的物件，不只是陳述，是附帶證明的陳述。每一行程式碼只是把之前的陳述拼起來建立新的陳述。想法不新，這些東西叫證明助手，提供語言讓你建立相當複雜的數學證明。它們產生證書，如果你信任 Lean 的編譯器，就 100% 保證你的論證正確。他們把編譯器做得很小，有幾種不同的 Lean 編譯器可用。 很多數學家參與了 Lean 的設計。設計成單獨程式碼行像單獨數學論證行。你可能想引入一個變數，想用反證法。有各種標準事情可以做，寫出來。理想情況下應該有一一對應。實際上不是，因為 Lean 在向一個極度挑剔的同事解釋證明，他會指出，你真的這個意思嗎？如果這是零會怎樣？你怎麼證明這個？Lean 有很多自動化來減少煩人程度。每個數學物件都必須有型別。如果我說 x，x 是實數還是自然數還是函式？寫非正式的，常常有上下文。你說顯然 x 等於，讓 x 是 y 和 z 的和，y 和 z 已經是實數，所以 x 也應該是實數。Lean 能做很多這樣的事，每隔一段時間它說，等等，你能告訴我更多關於這個物件是什麼嗎？什麼型別？你必須更哲學地思考，不只是你做的計算，每個物件在某種意義上實際是什麼。 Lean 用的是老式 AI，傳統的。你可以把所有東西表示成樹，總有演算法把一棵樹匹配到另一棵樹。每個物件都帶著它從哪來的歷史，你可以追溯。它設計是為了可靠性。現代 AI 不用在裡面，是分離的技術。人們開始在 Lean 之上使用 AI。數學家試圖在 Lean 裡程式設計證明，常常有一步，現在我想用微積分基本定理做下一步。Lean 開發者建了一個巨大的專案叫 Mathlib，幾萬條關於數學物件的有用事實的集合。某處有微積分基本定理，你需要找到它。很多瓶頸現在是引理搜尋。你知道某個工具在那裡，需要找到它。有專門的搜尋引擎，現在也有大語言模型，你可以說，我需要這個點的微積分基本定理。陶哲軒寫程式碼時裝了 GitHub Copilot 作為 IDE 外掛，掃描文字，看需要什麼。他可能打，現在我需要用微積分基本定理，然後它建議，試試這個。大約 25% 的時候完全正確，另外 10 到 50% 的時候不完全對，足夠接近，改改這裡那裡就行。一半的時候給完全垃圾。人們開始在上面用 AI，主要是在花哨自動補全的層面。 陶哲軒估計現在形式化一個證明所需的時間和精力大約是寫出來的 10 倍。可行，煩人。 這不就殺了當數學家的氛圍嗎？有個挑剔的同事。如果那是唯一的特性，確實。有些情況下正式地做事情實際上更愉快。他形式化過一個定理，最終陳述裡出現一個常數 12。這個 12 貫穿整個證明，一切都必須檢查，所有其他數字必須與最終數字 12 一致。他們寫了一篇論文。幾周後有人說，我們可以透過重做某些步驟把 12 改進到 11。這發生在紙筆上時，每次改變引數，你必須逐行檢查證明的每一行是否仍然有效。可能有微妙的事情，你沒意識到的某些性質，不是數字 12，你沒意識到你在利用。證明可能在微妙的地方崩潰。 他們用常數 12 形式化了證明。新論文出來後，他們說要更新到 11。用 Lean 你能做的，在主定理裡把 12 改成 11，執行編譯器，幾千行程式碼中，90% 仍然工作，有幾行標紅。我無法證明這些步驟，立刻隔離出你需要改變哪些步驟。你可以跳過一切正常工作的部分。如果你用好的程式設計實踐正確程式設計，大多數行不會紅。只有少數地方，如果你不硬編碼常數，用聰明的策略，你可以把需要改變的東西區域性化到很小的時間。一兩天內他們就更新了證明，過程收斂得比紙筆平滑得多。 證明更長，每一塊更容易讀。數學論文跳到第 27 頁看第六段，有一行數學文字，陶哲軒常常不能立刻讀懂，因為它假設了各種定義，你得回到十頁前看定義，證明散落各處，你被迫相當順序地讀。不像小說可以開啟中間開始讀，有很多上下文。在 Lean 裡，你把游標放在一行程式碼上，每個物件都可以懸停檢視，告訴你它是什麼，從哪來，哪裡的東西被證明。追溯比翻數學論文容易多了。 Lean 真正實現的一件事是可以在非常原子的尺度上合作證明，這在過去做不到。傳統紙筆，想和另一個數學家合作，要麼在黑板上互動，要麼透過郵件，基本必須分段，我完成第三節，你做第四節。你沒法真正同時做同一件事。用 Lean，你可以試著形式化證明的某部分，說我在第 67 行卡住了，我需要證明這個，不太行，這是我遇到麻煩的三行程式碼。因為所有上下文都在，別人可以說，我認出你需要做什麼，你需要應用這個技巧或工具。你可以進行極其原子級別的對話。因為 Lean，陶哲軒能和全世界幾十個人合作，大多數他從未見過面，他甚至可能不知道他們在證明領域有多可靠。Lean 給他信任的證書，所以他能做無信任數學。 陶哲軒以偉大的合作者著稱。合作解決困難數學問題的正確方式是什麼？數學研究專案本質上是，開始時你不知道怎麼做。不像工程專案，理論已經建立幾十年，主要困難是實現。你必須搞清楚正確的路徑是什麼。這就是他說的先作弊。回到建橋的類比。先假設你有無限預算、無限勞動力，現在你能建這座橋嗎？現在有無限預算但有限勞動力，現在能嗎？當然沒有工程師能這樣做，他們有固定需求。一開始總有這樣的即興演奏，你嘗試各種瘋狂的東西，做各種不現實的假設，計劃稍後修正。你試圖看是否有某個方法的骨架可能行得通。希望這能把問題分解成更小的子問題，你不知道怎麼做，專注於子問題。有時不同的合作者更擅長某些事情。 他的一個主題是本·格林，現在叫格林-陶定理。素數包含任意長度的等差數列。這是他修改塞邁雷迪定理的結果。他們合作的方式是，本已經證明了長度三的類似結果，他的技術只適用於三。陶哲軒有遍歷理論的技術，他當時比本更熟悉。如果他能證明素數相關的某個集合的某些隨機性性質，某個技術條件，如果本能提供這個事實，他就能推出定理。他要求的是數論中非常困難的問題，本說沒辦法證明。所以他說，你能用我有一個機會證明的弱假設來證明你那部分嗎？他提出了他能證明的東西，對陶哲軒太弱了。我無法用這個。來回對話，一個駭客。我想作弊更多，他想作弊更少。最終他們找到一個性質，本能證明，陶哲軒能用，然後他們能證明定理。每種合作都有故事，沒有兩個一樣。 有了 Lean，這幾乎是另一個故事。你可以為一個問題建立藍圖，真正做分而治之，在不同的部分工作，用計算機證明檢查器確保一切正確。它讓一切相容、可信任。目前只有少數數學專案能這樣切分。當前最先進的狀態，大多數 Lean 活動是形式化已經被人類證明的證明。數學論文基本上是一種藍圖。把困難陳述分解成一百個小引理，往往沒有寫得足夠詳細，每個都能直接形式化。藍圖是論文的極度挑剔版本，每一步儘可能詳細解釋，讓每一步自包含，或只依賴於非常特定數量的已證明的先前陳述。這樣生成的藍圖圖的每個節點可以獨立於其他節點處理。你甚至不需要知道整個東西如何工作。像現代供應鏈。想造 iPhone 或其他複雜東西，沒有一個人能造整個東西，可以有專家，給他們來自其他公司的零件，他們能把它們組合成一個稍大的零件。 這是令人興奮的可能性。如果能找到能這樣分解的問題，可以有幾千個貢獻者。完全分散式。 陶哲軒之前講過理論數學和實驗數學的分裂。現在大多數數學是理論的，只有一小部分是實驗的。他認為 Lean 和其他軟體工具，GitHub 之類，會讓實驗數學擴大到比現在大得多的程度。現在想做某個數學模式或東西的數學探索，你需要一些程式碼寫出模式。有時有計算機代數包能幫忙，常常只是一個數學家寫大量的 Python 或其他。因為編碼是如此容易出錯的活動，讓其他人和你合作寫模組不現實，如果一個模組有 bug，整個東西不可靠。所以你得到非專業程式設計師寫的定製的義大利麵條式程式碼，笨重緩慢。因此很難大量生產實驗結果。 有了 Lean，他已經開始一些專案，不只是實驗資料，是實驗證明。他有個叫等式理論專案的專案。生成了大約 2200 萬個抽象代數的小問題。抽象代數研究乘法、加法這樣的運算和抽象性質。乘法是交換的，x 乘 y 總是 y 乘 x，至少對數字是這樣。也是結合的，x 乘 y 乘 z 和 x 乘 y 乘 z 一樣。這些運算服從某些定律，不服從另一些。比如 x 乘 x 不總是等於 x，這條定律不總是成立。給定任何運算，它服從某些定律，不服從另一些。他們生成了大約 4000 條可能的代數定律。問題是哪些定律蘊含哪些其他定律。比如交換性蘊含結合性嗎？答案是否定的，因為你可以描述一個服從交換律但不服從結合律的運算。透過給出例子，你能證明交換性不蘊含結合性。有些定律確實透過替換之類蘊含其他定律，你可以寫下代數證明。他們看這 4000 條定律之間的所有配對，多達 2200 萬個。對每個配對，問這條定律蘊含這條嗎？如果是，給證明。如果不是，給反例。2200 萬個問題，每個都可以給本科代數學生，他們有不錯的機會解決，有一些，大約一百個，真的相當難，很多是簡單的。專案就是確定整個圖，哪些蘊含哪些。 這不可行，文獻中的最先進水平大約是 15 個方程，是紙筆人類能做到的極限。你需要擴大規模。需要眾包，也需要信任，沒有人能檢查 2200 萬個證明。需要計算機化。只有 Lean 才可能。他們希望也用很多 AI。專案幾乎完成了。2200 萬個裡，除了兩個都解決了。實際上那兩個有紙筆證明，正在形式化。陶哲軒早上還在做，快完成了。大約 50 人參與，在數學裡被認為是巨大的數字。會有 50 個作者的論文，一個大附錄說明誰貢獻了什麼。 組織貢獻時可以按專業水平嗎？可以有 ELO 評分之類的遊戲化嗎？Lean 專案的美妙之處在於自動獲得所有這些資料，所有東西上傳到 GitHub。GitHub 追蹤誰貢獻了什麼。你可以生成統計。這些是很粗糙的指標。陶哲軒絕對不希望這成為終身教職評審的一部分。在企業計算中，人們已經用一些這樣的指標評估員工表現。這是學術圈有點可怕的方向，我們不太喜歡指標。 但學術圈用指標，只是用舊的，論文數量。這確實。這是個指標，雖然有缺陷，方向更正確。有趣，至少很有趣。你可以研究這些是否更好的預測器。有個問題叫古德哈特定律。如果一個統計量被用來激勵表現，它會被博弈，然後不再是有效的度量。人類總是博弈。這是理性的。 他們專案做的是自我報告。有科學界的標準類別，什麼型別的貢獻。概念和驗證、資源、編碼等等。有大約 12 個類別的標準列表。他們讓每個貢獻者在作者和類別的矩陣裡勾選他們認為自己貢獻的地方，給個粗略想法。你做了些編碼，提供了些算力，沒做紙筆驗證。這行得通。傳統上數學家按姓氏字母排序，沒有科學界的第一作者、第二作者傳統，他們為此自豪。所有作者地位平等。這不適用於這麼大的規模。 十年前他參與過博學專案，眾包數學但沒有 Lean 元件。受限於需要人類版主檢查所有貢獻是否有效。這是巨大的瓶頸。仍有大約 10 個作者的專案。當時他們決定不試圖決定誰做了什麼，用一個筆名。他們創造了一個虛構角色叫 DHJ 博學，向 20 世紀著名數學家群體的筆名致敬。論文署名這個筆名，我們都沒得到作者信用。這後來證明不太好，有兩個原因。一是如果你想被考慮終身教職，你不能用這篇論文作為你的出版物，因為它沒有正式作者信用。另一個他們後來認識到的是，當人們提到這些專案時，他們自然提到參與的最著名的人。這是蒂姆·高爾斯的博學專案，這是陶哲軒的博學專案，不提其他 19 個人。這次他們嘗試不同的，每個人都是作者，會有附錄有這個矩陣，看看效果如何。 ## AI 與數學：合作還是替代 DeepMind 的 AlphaProof 用強化學習在失敗的成功的 Lean 形式化證明上訓練，解決 IMO 問題。非常高中的水平。陶哲軒怎麼看？難度隨證明涉及的步數指數增長。組合爆炸。大語言模型會犯錯，如果證明有 20 步，每一步有 10% 的失敗率走錯方向，極不可能到達終點。 從自然語言對映到形式化程式有多難？極其困難。自然語言容錯性很強。你可以犯些小語法錯誤，用第二語言說，別人能大致理解。形式語言，一個小錯誤，整個東西就是無意義的。即使形式到形式也很難。有不同的不相容的字首和語言。有 Lean，還有 Coq 和 Isabelle。即使從一個形式語言轉換到另一個形式語言也是未解決的問題。 AlphaProof 令人印象深刻，顯示了什麼是可能的。方法目前不能擴充套件。三天的谷歌伺服器時間能解決一個高中數學題。這不是可擴充套件的前景，特別是隨複雜度指數增長。 他們得了銀牌表現。首先，他們用了比規定多得多的時間，有人類幫助形式化，還給自己滿分，因為是形式化驗證的。所以公平。有努力，會有提案在某個時候真正舉辦 AI 數學奧林匹克，同時給人類參賽者和 AI 同樣的題目，同樣的時間，輸出由同樣的評委評分，這意味著必須用自然語言而不是形式語言寫。 希望這會發生。不會在這次 IMO 發生，時間段內表現不夠好。有更小的比賽，答案是數字而不是長形式證明的比賽。AI 在特定數值答案的問題上好得多，因為容易做強化學習。你答對了，你答錯了，訊號很清楚。長形式證明要麼必須形式化，然後 Lean 給贊或踩，要麼非形式化，然後需要人類告訴。如果你試圖做幾十億次強化學習執行，你僱不起足夠的人類來評分。讓大語言模型在普通文字上做強化學習已經夠難了。現在你真的僱人，不只是點贊點踩，而是數學上檢查輸出，太貴了。 人類在數學裡做的最特別的事，AI 短期內無法突破的是什麼？發明新理論？提出新猜想還是證明猜想？構建新抽象？新表示？還是看到不同領域之間的新聯絡？ 數學家的本質隨時間變化很大。一千年前，數學家必須計算復活節日期，非常複雜的計算，已經自動化幾個世紀了，我們不再需要。他們曾經做球面導航，圓三角學，從舊世界到新世界怎麼走，非常複雜的計算。也已經自動化。甚至很多本科數學，在 AI 之前，比如 Wolfram Alpha，不是語言模型，能解決很多本科水平的數學任務。計算那一塊，驗證例行事情，比如有一個偏微分方程問題，你能用 20 個標準技術中的任何一個解決嗎？說，是的，我試了所有 20 個，這裡有 100 個不同的排列和我的結果。這類事情會工作得很好，擴充套件到一旦你解決一個問題，讓 AI 攻擊一百個相鄰問題。 人類仍然做的。AI 現在真正掙扎的是知道什麼時候走錯了路。它可以說，我要解決這個問題，把它分成兩種情況，試試這個技術。有時如果你幸運，問題簡單，是正確技術，解決了問題。有時它會提出一個方法，完全是胡說八道，看起來像證明。 LLM 生成的數學有一個煩人的地方。人類生成的數學質量很低，比如沒有正式訓練的投稿，如果人類證明是壞的，你很快能看出來，犯很基本的錯誤。AI 生成的證明，表面上看可能完美無瑕。部分因為強化學習實際訓練它們做的是產生看起來正確的東西，對很多應用來說足夠好。錯誤往往非常微妙，當你發現時，非常愚蠢。沒有人類會犯那種錯誤。 程式設計情境下很令人沮喪。人類寫低質量程式碼時，有程式碼味道，你能立刻看出跡象。AI 生成的程式碼，最終你發現一個明顯愚蠢的東西，只是看起來像好程式碼。很棘手，很令人沮喪。 嗅覺，這是人類有的一樣東西。有一種比喻性的數學嗅覺，不清楚如何讓 AI 複製。AlphaZero 在國際象棋和圍棋中取得進展的方式，某種意義上它們發展出了對棋局位置的嗅覺，這個位置對白方好，對黑方好。它們無法解釋為什麼，有了那個嗅覺就能制定策略。如果 AI 獲得判斷某些證明策略可行性的能力，因為我打算把這個問題分成兩個小任務，它們能說，這看起來好，兩個任務看起來比主任務簡單，仍有很好機會是真的，所以值得試。或者，不，你把問題弄得更糟了，因為兩個子問題實際上都比原問題難。這實際上是如果你隨機試一件事通常會發生的事情，非常容易把問題轉換成更難的問題。很少轉換成更簡單的問題。如果它們能獲得嗅覺，也許能開始競爭人類水平的數學家。 如果給陶哲軒一個神諭，能做他做的某方面，他願意合作，希望神諭能做什麼？他希望是驗證器，檢查，是的，陶教授，正確，這是有希望的方向？還是生成可能的證明然後他看哪個對？還是生成不同的表示，完全不同的看問題的方式？ 所有上述。很多是我們不知道如何使用這些工具，因為這是過去沒有過的正規化。系統足夠勝任理解複雜指令，能在巨大規模上工作，不可靠。有趣的是，在微妙的方式上不可靠，同時提供足夠好的輸出。有趣的組合。你有研究生和你合作，有點像這樣，不是規模。我們之前有能大規模工作的軟體工具，非常窄。我們必須搞清楚如何使用。蒂姆·高爾斯在 2000 年就預見到了。他在展望 25 年後數學會是什麼樣。他寫了一篇文章，一個未來的數學助手和他自己的假設對話。他試圖解決一個問題，他們對話。有時人類提個想法，AI 評估，有時 AI 提個想法。有時需要計算，AI 就去說，好，我檢查了這裡需要的 100 個情況，或者你為所有 n 設定這個，我檢查了 n 到 100，看起來好，或者等等，n 等於 46 有問題。自由形式的對話，你事先不知道事情會走向哪裡，基於，我想想法雙方都會提。計算雙方都會提。 陶哲軒和 AI 有過對話，他說，我們合作解決這個數學問題。是一個他已經知道答案的問題，他試著提示。好，這是問題。我建議用這個工具，它會找到這個。它可能開始用這個，然後回到它之前想做的工具。你必須不斷把它引到你想要的路上。他最終能強迫它給出他想要的證明，像趕貓。他必須付出的個人努力，不只是提示它，還檢查輸出，因為很多看起來會成功，他知道第 17 行有問題，和它爭論。比無輔助地做更累。這是當前最先進的狀態。 會不會有一個相變，不再感覺像趕貓。陶哲軒相信會。在形式化中，他之前提到形式化一個證明比手寫多花 10 倍時間。有了現代 AI 工具和更好的工具，Lean 開發者做得很好，加更多功能，讓它使用者友好，從 9 降到 8 降到 7。沒什麼大不了，有一天會降到 1。那是相變，因為突然寫論文先用 Lean 寫，或者透過和 AI 對話，一般和你實時進行，就變得自然了。期刊接受也變得自然。也許提供快速審稿。如果論文已經用 Lean 形式化，他們只讓審稿人評論結果的重要性和與文獻的聯絡，不太擔心正確性，因為已經被認證了。論文越來越長，越來越難得到好的審稿，除非非常重要。這實際是個問題，形式化來得正是時候。 更簡單更容易，因為工具和其他因素，你會看到 Mathlib 可能指數增長，良性迴圈。一個這樣的相變過去發生過，LaTeX 的採用。LaTeX 是所有數學家現在用的排版語言。過去人們用各種文書處理器和打字機，某個時候 LaTeX 變得比其他競爭對手更容易用，人們幾年內就切換了。戲劇性的相變。 多遠的未來，AI 系統能作為合作者參與贏得菲爾茲獎的證明？這取決於合作的程度。已經是了。他能想象一篇獲獎論文有 AI 輔助寫作，就像 Copilot 已經加速他自己的寫作。你有一個定理和一個證明，證明有三種情況，我寫下第一種情況的證明，自動補全建議，現在第二種情況的證明可能這樣。完全正確。很好。節省了五到十分鐘的打字。 那種情況 AI 不會得菲爾茲獎。是 20 年，50 年，100 年？陶哲軒印出的預測是到 2026 年，就是明年，會有數學和 AI 的合作，不是菲爾茲獎級別的，是實際研究級論文。也許不是想法，至少一些計算、驗證。已經發生了。有些問題透過和 AI 對話提出東西的複雜過程解決，人類去試，合約不成功，它可能提出不同的想法。很難精確區分。確實有數學結果只能因為有人類認證和 AI 參與才能完成，很難區分功勞。這些工具不復制數學所需的所有技能，能複製相當大比例，30%、40%，能填補空白。編碼是好例子。陶哲軒用 Python 編碼很煩，他不是職業程式設計師，有了 AI，摩擦成本大大降低。填補了那個空白。AI 在文獻綜述上變得相當好。仍然有幻覺引用不存在的問題，這可以解決。如果以正確的方式訓練，用網際網路驗證，幾年內能達到，你有一個需要的引理，說有人證明過嗎？它會做花哨的網頁搜尋，說，是的，有六篇論文有類似的東西。現在你可以問它，它給你六篇，其中一篇合法相關，一篇存在但不相關，四篇是幻覺。現在成功率非零，垃圾太多，訊雜比太差，最有幫助的是當你已經大致知道關係，只需要被提醒一個已經潛意識在記憶裡的論文。而不是幫你發現你完全不知道但正確的新引用。它有時能，被埋在一堆選項中，其他的都是壞的。能自動生成正確的相關工作部分，這是美麗的事情。可能是另一個相變，因為它正確分配信用。打破思想孤島。 現在有很大障礙。像自動駕駛。安全邊際必須很高才可行。很多 AI 應用有明天問題，能開發工作 20%、80% 時間的工具，還不夠好。實際上，有時比好更糟。 另一種問菲爾茲獎問題的方式，哪一年你會醒來真的很驚訝，讀新聞，AI 做了真正的突破。這個十年他能看到它在人們認為不相關的兩個東西之間建立聯絡。生成一個猜想，有真正的機會正確和有意義。當前模型很掙扎。物理學家有一個夢想，讓 AI 發現新的物理定律。夢想是餵它所有資料，這是新規律。實際上，當前最先進的狀態甚至難以從資料中發現舊的物理定律。如果它做到了，有個大擔憂是汙染，它只是因為在訓練裡才有。部分是我們沒有正確的訓練資料。對於物理定律，我們沒有一百萬個不同宇宙有一百萬個不同自然定律。數學中缺失的很多實際上是負空間。我們有已發表的人們能證明的東西，最終被驗證的猜想或產生反例，我們沒有資料關於那些被提出，是好的嘗試，人們很快意識到是錯誤猜想，然後說，哦，但我們應該改變我們的聲稱，以這種方式