用AI工具輔助研究數學的項目，再一次被陶哲軒跑通！

三周前，他曾發布一篇博文，記錄下自己使用Blueprint在Lean4中形式化多項式Freiman-Ruzsa猜想的證明過程。

就在昨天，他激動宣布：將多項式Freiman-Ruzsa猜想的證明形式化的Lean4項目，在三周后取得了成功！

現在，依賴關系圖已經完全被綠色所覆蓋，Lean編譯器也報告說，這個猜想完全遵循標準公理。

陶哲軒表示，在整個團隊中，自己貢獻的代碼大概只有5%。這個結果很鼓舞人心，因為這意味著數學家即使不具備Lean編程技能，也能領導Lean的形式化項目。

他發現，項目中在數學上最有趣的部分，形式化起來比較容易，而技術上看起來最顯而易見的步驟，卻最耗時。

而使用Blueprint將項目分解成難度小到中等的部分，效果很好，這就讓大量并行工作成為可能。

這樣，許多貢獻者就可以處理特定的子任務，而無需理解整個證明過程，甚至可以完全不了解相關的數學領域知識。

就在幾分鐘前，Lean成功證明了PFR猜想，且沒有留下任何懸而未決的問題（后文將會提到的「sorry」）。這意味著，這個項目的所有主要目標，都已經圓滿完成。

與此同時，他在三周前也就是11月18日的那篇博客也被網友翻出，引發熱議。

果然，AI加持數學研究顛覆力量的后勁，得需要數月的時間才能讓人們認識到。

而只有在最前線的研究者，才能在第一時間切實感覺到這種巨大力量的沖擊和震撼。

陶哲軒呼吁：數學家們一定要學會用AI了

有網友向陶哲軒提問：這是否意味著，有越來越多的證明是人類不可理解，但機器可解決的？

陶哲軒表示，恰恰相反，如果證明的形式化變得更加主流，并且更多地得到AI輔助，那完全有可能創建出既人類可讀、又能被機器閱讀的證明。

PFR證明的blueprint就證明了這一點——既人類可讀，每個證明步驟還帶有形式化的理由，還能得到一個依賴關系圖，來可視化整個論證的全局結構。

當然，陶哲軒也提醒道，不要把「計算機輔助證明」和「不能提供理解/偶然成立的證明」搞混了。

比如對于有限單群分類的超過10000頁的證明，幾乎百分百是由人工生成的，但一個由計算機協助處理的替代證明，在某些方面看更令人滿意。

跟網友經過幾輪討論后，陶哲軒做出以下總結——

Blueprint本身就是一種編程語言，可以看作一種Lean的偽代碼。

許多數學家都應該將寫作風格從標準數學英語/LaTex，轉換為Blueprint/LaTex。

網友：以后研究都不需要「人類可讀」，AI懂就行了

網友表示，陶哲軒對于各種研究工具隨意掌握的程度，幾乎可以稱得上是可怕。

我在研究生階段對數學的嘗試，就就好像一個穴居人本來在搖晃一輛普通的獨輪車，忽然眼前出現了一輛直升機，上面的人向我伸出手，告訴我來試試看，一點也不可怕。

自從聽說四色定理以來，我一直很清楚，形式化是數學的未來。但我沒有預料到的是，陶哲軒如此從容不迫，形式化才剛剛獲得牽引力，他就能用AI完成幾乎所有的數學寫作。

形式化，是指從基本公理和規則中真正推導出證明中的每個陳述。而陶哲軒在這篇博文里，把需要死記硬背的勞動都抽象出來，交給了機器。

他的工作表明，形式化才剛剛開始在主流數學中受到關注。

已經有人開始暢想：很可能會有一段時間，大多數證明只是在Lean或類似系統中完成，再也沒有人需要費心寫一篇「人類可讀」的論文了。

數學，將變成一種編程！

一位數學碩士表示，現在自己的研究步驟有三步——

1.理解自己想證明的東西，通過閱讀或者與人交談；

2.用紙筆繪制出包含要點的草圖；

3.將校樣輸入到LaTeX中，讓自己要交的作業變得人類可讀。

是的，如果我們只是要訓練或微調AI來產生答案，然后編寫一個循環來反饋，直到編譯器正確輸出，那我們自己并不需要真的理解。

用這種方法，我們還能生成更多的訓練示例，可以手動檢查結果是否符合要求，做上注釋。而訓練，可以提高初始答案的準確性。

PFR猜想的形式化過程

以下是陶哲軒發在博客上的形式化過程，感興趣的讀者可以挑戰一下。

11月，陶哲軒與Yael Dillies和Bhavik Mehta啟動了一個合作項目，目的是利用Lean4對自己之前關于Freiman-Ruzsa（PFR）猜想的預印本論文進行形式化。

項目雖然啟動不到一周，但進展相當順利，大部分文件都被形式化了。

這個項目得益于Patrick Massot的Blueprint工具，這個工具讓團隊能夠編寫與Lean形式化緊密相關的、人類可讀的證明「藍圖」。

在Blueprint中，有一個陶哲軒特別喜歡的功能，那就是自動生成的依賴圖。它可以提供形式化進度的大致快照。截至當時，依賴圖的樣子如下：

在依賴圖的圖例中，不同的氣泡（表示引理）和矩形（表示定義）被賦予了不同的顏色。

簡單來說，綠色的氣泡或矩形表示那些已經被完全形式化的引理或定義，而藍色的則指那些已準備好進行形式化的引理或定義（這意味著它們的陳述已經形式化，但證明還沒有，同時所有相關的前置引理和證明也是如此）。

而陶哲軒團隊的目標，就是將所有通向「pfr」氣泡的底部氣泡，都變成綠色。

點擊依賴圖底部的「pfr」氣泡時，可以看到以下內容：

圖中，Blueprint顯示出一種人類可讀的PFR語句形式，還附帶了這個語句的人類可讀證明，該證明依賴于項目中的其他語句：

注意，「pfr」氣泡是白色的，但有一個綠色邊框，這意味著PFR的陳述已經在Lean中正式化，然而證明并沒有。

證明本身還沒有準備好被形式化，是因為一些先決條件（特別是「entropy-pfr」Theorem 6.16）甚至還沒有形式化的陳述。

單擊依賴關系圖中PFR陳述下方的Lean鏈接，就可以進入相應的Lean文檔：

這就是Lean中的典型定理的樣子。在冒號之前有許多假設，例如：

G是一個屬于順序2的有限初等阿貝爾群 （這就是團隊選擇形式化有限場向量空間的方式）；A是G的非空子集；A+A的基數＜K倍A的基數。

冒號后邊的陳述是結論：A可以以c+H的和的形式包含在G的子群H中，以及在最多的基數的集合c中。

聰明的讀者可能會注意到，上面的定理似乎缺少一兩個細節，例如，它沒有明確斷言H是一個子群。

這是因為「pretty printing」模式抑制了定理陳述中的一些信息，只要單擊「來源」鏈接，就可以看到了。

可以看到，H需要具有G加法子群的類型。

該定理底部有一個明顯的「sorry」，這意味著尚未為該定理提供證明，但最終意圖當然是用實際證明，來代替這個「sorry」。

填補這個「sorry」現在還很難做到，所以需要尋找一個更簡單的任務。

下面是一個簡單的中間引理「ruzsa-nonneg」，它出現在證明中：

該表達式指的是X和Y之間的熵Ruzsa距離，它是一個實數。

氣泡是藍色的，帶有綠色邊框，這意味著陳述已經形式化，證明也準備好形式化了。

Blueprint依賴關系圖表明，這個引理可以從前面的一個引理中推導出來，稱為「ruzsa-diff」：

「uzsa-diff」也是藍色的，邊框是綠色的，所以它與「ruzsa-nonneg」具有相同的當前狀態：陳述是形式化的，證明也準備好形式化了，但證明還沒有用Lean編寫。其中，是X的香農熵。

通過觀察Lemma 3.11和Lemma 3.13，我們可以清楚地看到|H[X] - H[Y]|顯然是非負的。

因此，即使我們還不知道如何證明Lemma 3.11，但假設Lemma 3.11成立，并補全Lemma 3.13的證明，應該是輕而易舉的事。

Lemma 3.11的形式化如下：（「sorry」表示Lemma目前還沒有證明）

同時，Lemma 3.13的形式化為：

現在，我們要試著把后一個「sorry」填上。

在PFR github倉庫的本地副本中，陶哲軒用編輯器（Visual Studio Code，擴展名為lean4）打開了相關的Lean文件，并導航到「rdist_nonneg」的「sorry」處。

隨附的「Lean信息視圖」就會顯示Lean證明的當前狀態：

在底部，可以看到我們需要證明的目標。

接下來，在證明這個說法時，需要運用一系列「戰術」來改變目標和/或假設。

第一步是加入應用Lemma 3.11所需的因子2。

現在，我們有了兩個目標（和兩個「sorry」）：一個是證明等價于；另一個是證明。

在填上第一個「sorry」之后的狀態如下（刪去了一些無關的假設）：

這里可以使用一種非常方便的「linarith」策略，它能解決任何可以通過現有假設的線性運算得出的目標：

成功之后可以看到，狀態報告顯示這個分支已經沒有需要證明的目標了。所以，我們繼續剩下的「sorry」，也就是證明：

在這里，我們將嘗試引用Lemma 3.11。為此，陶哲軒添加了幾行代碼：

于是，我們又有了兩個子目標，一個是證明約束（可以稱之為「h」），另一個是就從h推導出前一個目標。

對于第一個目標，需要調用正在編碼Lemma 3.11的「diff_ent_le_rdist」引理。

其中一種方法是嘗試使用「exact? 」策略，它會自動搜索，看目標是否可以立即從現有的引理中推導出來：

于是，陶哲軒點擊了建議的代碼（系統會自動將其粘貼到正確的位置）。結果成功了，只留下最后的「sorry」：

這里，陶哲軒通用使用了「exact?」策略，并按照它的建議建立匹配了邊界：

在補全最后一個「sorry」時，陶哲軒再一次嘗試了「exact?」，想知道如何把h和h'結合起來才能達到預期目標，結果成功了！

可以看到，所有的下劃線都消失了。也就是說，Lean已將其視為有效證明。

通過省略幾個中間步驟，我們可以將這個證明壓縮得相當緊湊：

現在證明完成了！

我們最后得到的，基本就是一個「單線證明」，考慮到Lemma 3.11和Lemma 3.13是如此接近，這也是合情合理的。

然后，陶哲軒將所有內容推送回Github主版本庫。

Blueprint的重建需要相當長的時間（約半小時），依賴關系圖現在以綠色顯示 「ruzsa-nonneg」：

因此可以說，PFR的形式化更接近完成了。

不過，雖然「ruzsa-nonneg」現在被涂成綠色，但還沒有這個結果的完整證據，因為它所依賴的引理「ruzsa-diff」不是綠色的。

從這一點上看，證明仍然是局部完成的。

陶哲軒表示，希望在未來的某個時候，前身結果也能被證明，那時，就可以說PFR猜想的結果，得到了完全的證明。