【新智元導讀】歷時三周，陶哲軒成功地用 AI 工具完成了形式化多項式 Freiman-Ruzsa 猜想證明過程的工作。他再次呼吁數(shù)學研究者學會正確利用 AI 工具，網(wǎng)友驚呼：以后的數(shù)學論文不需要人類可讀了？
用 AI 工具輔助研究數(shù)學的項目，再一次被陶哲軒跑通！
三周前，他曾發(fā)布一篇博文，記錄下自己使用 Blueprint 在 Lean4 中形式化多項式 Freiman-Ruzsa 猜想的證明過程。
就在昨天，他激動宣布：將多項式 Freiman-Ruzsa 猜想的證明形式化的 Lean4 項目，在三周后取得了成功！
現(xiàn)在，依賴關系圖已經(jīng)完全被綠色所覆蓋，Lean 編譯器也報告說，這個猜想完全遵循標準公理。
陶哲軒表示，在整個團隊中，自己貢獻的代碼大概只有 5%。這個結果很鼓舞人心，因為這意味著數(shù)學家即使不具備 Lean 編程技能，也能領導 Lean 的形式化項目。
他發(fā)現(xiàn)，項目中在數(shù)學上最有趣的部分，形式化起來比較容易，而技術上看起來最顯而易見的步驟，卻最耗時。
而使用 Blueprint 將項目分解成難度小到中等的部分，效果很好，這就讓大量并行工作成為可能。
這樣，許多貢獻者就可以處理特定的子任務，而無需理解整個證明過程，甚至可以完全不了解相關的數(shù)學領域知識。
就在幾分鐘前，Lean 成功證明了 PFR 猜想，且沒有留下任何懸而未決的問題（后文將會提到的「sorry」）。這意味著，這個項目的所有主要目標，都已經(jīng)圓滿完成。
與此同時，他在三周前也就是 11 月 18 日的那篇博客也被網(wǎng)友翻出，引發(fā)熱議。
果然，AI 加持數(shù)學研究顛覆力量的后勁，得需要數(shù)月的時間才能讓人們認識到。
而只有在最前線的研究者，才能在第一時間切實感覺到這種巨大力量的沖擊和震撼。
陶哲軒呼吁：數(shù)學家們一定要學會用 AI 了
有網(wǎng)友向陶哲軒提問：這是否意味著，有越來越多的證明是人類不可理解，但機器可解決的？
陶哲軒表示，恰恰相反，如果證明的形式化變得更加主流，并且更多地得到 AI 輔助，那完全有可能創(chuàng)建出既人類可讀、又能被機器閱讀的證明。
PFR 證明的 blueprint 就證明了這一點 —— 既人類可讀，每個證明步驟還帶有形式化的理由，還能得到一個依賴關系圖，來可視化整個論證的全局結構。
當然，陶哲軒也提醒道，不要把「計算機輔助證明」和「不能提供理解 / 偶然成立的證明」搞混了。
比如對于有限單群分類的超過 10000 頁的證明，幾乎百分百是由人工生成的，但一個由計算機協(xié)助處理的替代證明，在某些方面看更令人滿意。
跟網(wǎng)友經(jīng)過幾輪討論后，陶哲軒做出以下總結 ——
Blueprint 本身就是一種編程語言，可以看作一種 Lean 的偽代碼。
許多數(shù)學家都應該將寫作風格從標準數(shù)學英語 / LaTex，轉(zhuǎn)換為 Blueprint / LaTex。
網(wǎng)友：以后研究都不需要「人類可讀」，AI 懂就行了
網(wǎng)友表示，陶哲軒對于各種研究工具隨意掌握的程度，幾乎可以稱得上是可怕。
我在研究生階段對數(shù)學的嘗試，就就好像一個穴居人本來在搖晃一輛普通的獨輪車，忽然眼前出現(xiàn)了一輛直升機，上面的人向我伸出手，告訴我來試試看，一點也不可怕。
自從聽說四色定理以來，我一直很清楚，形式化是數(shù)學的未來。但我沒有預料到的是，陶哲軒如此從容不迫，形式化才剛剛獲得牽引力，他就能用 AI 完成幾乎所有的數(shù)學寫作。
形式化，是指從基本公理和規(guī)則中真正推導出證明中的每個陳述。而陶哲軒在這篇博文里，把需要死記硬背的勞動都抽象出來，交給了機器。
他的工作表明，形式化才剛剛開始在主流數(shù)學中受到關注。
已經(jīng)有人開始暢想：很可能會有一段時間，大多數(shù)證明只是在 Lean 或類似系統(tǒng)中完成，再也沒有人需要費心寫一篇「人類可讀」的論文了。
數(shù)學，將變成一種編程！
一位數(shù)學碩士表示，現(xiàn)在自己的研究步驟有三步 ——
1.理解自己想證明的東西，通過閱讀或者與人交談；
2.用紙筆繪制出包含要點的草圖；
3.將校樣輸入到 LaTeX 中，讓自己要交的作業(yè)變得人類可讀。
是的，如果我們只是要訓練或微調(diào) AI 來產(chǎn)生答案，然后編寫一個循環(huán)來反饋，直到編譯器正確輸出，那我們自己并不需要真的理解。
用這種方法，我們還能生成更多的訓練示例，可以手動檢查結果是否符合要求，做上注釋。而訓練，可以提高初始答案的準確性。
PFR 猜想的形式化過程
以下是陶哲軒發(fā)在博客上的形式化過程，感興趣的讀者可以挑戰(zhàn)一下。
11 月，陶哲軒與 Yael Dillies 和 Bhavik Mehta 啟動了一個合作項目，目的是利用 Lean4 對自己之前關于 Freiman-Ruzsa（PFR）猜想的預印本論文進行形式化。
項目雖然啟動不到一周，但進展相當順利，大部分文件都被形式化了。
這個項目得益于 Patrick Massot 的 Blueprint 工具，這個工具讓團隊能夠編寫與 Lean 形式化緊密相關的、人類可讀的證明「藍圖」。
在 Blueprint 中，有一個陶哲軒特別喜歡的功能，那就是自動生成的依賴圖。它可以提供形式化進度的大致快照。截至當時，依賴圖的樣子如下：
在依賴圖的圖例中，不同的氣泡（表示引理）和矩形（表示定義）被賦予了不同的顏色。
簡單來說，綠色的氣泡或矩形表示那些已經(jīng)被完全形式化的引理或定義，而藍色的則指那些已準備好進行形式化的引理或定義（這意味著它們的陳述已經(jīng)形式化，但證明還沒有，同時所有相關的前置引理和證明也是如此）。
而陶哲軒團隊的目標，就是將所有通向「pfr」氣泡的底部氣泡，都變成綠色。
點擊依賴圖底部的「pfr」氣泡時，可以看到以下內(nèi)容：
圖中，Blueprint 顯示出一種人類可讀的 PFR 語句形式，還附帶了這個語句的人類可讀證明，該證明依賴于項目中的其他語句：
注意，「pfr」氣泡是白色的，但有一個綠色邊框，這意味著 PFR 的陳述已經(jīng)在 Lean 中正式化，然而證明并沒有。
證明本身還沒有準備好被形式化，是因為一些先決條件（特別是「entropy-pfr」Theorem 6.16）甚至還沒有形式化的陳述。
單擊依賴關系圖中 PFR 陳述下方的 Lean 鏈接，就可以進入相應的 Lean 文檔：
這就是 Lean 中的典型定理的樣子。在冒號之前有許多假設，例如：
G 是一個屬于順序 2 的有限初等阿貝爾群 （這就是團隊選擇形式化有限場向量空間的方式）；A 是 G 的非空子集；A+A 的基數(shù)＜K 倍 A 的基數(shù)。
冒號后邊的陳述是結論：A 可以以 c+H 的和的形式包含在 G 的子群 H 中，以及在最多 2K12 的基數(shù)的集合 c 中。
聰明的讀者可能會注意到，上面的定理似乎缺少一兩個細節(jié)，例如，它沒有明確斷言 H 是一個子群。
這是因為「pretty printing」模式抑制了定理陳述中的一些信息，只要單擊「來源」鏈接，就可以看到了。
可以看到，H 需要具有 G 加法子群的類型。
該定理底部有一個明顯的「sorry」，這意味著尚未為該定理提供證明，但最終意圖當然是用實際證明，來代替這個「sorry」。
填補這個「sorry」現(xiàn)在還很難做到，所以需要尋找一個更簡單的任務。
下面是一個簡單的中間引理「ruzsa-nonneg」，它出現(xiàn)在證明中：
該表達式 d【X;Y】指的是 X 和 Y 之間的熵 Ruzsa 距離，它是一個實數(shù)。
氣泡是藍色的，帶有綠色邊框，這意味著陳述已經(jīng)形式化，證明也準備好形式化了。
Blueprint 依賴關系圖表明，這個引理可以從前面的一個引理中推導出來，稱為「ruzsa-diff」：
「uzsa-diff」也是藍色的，邊框是綠色的，所以它與「ruzsa-nonneg」具有相同的當前狀態(tài)：陳述是形式化的，證明也準備好形式化了，但證明還沒有用 Lean 編寫。其中，H【X】是 X 的香農(nóng)熵。
通過觀察 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 的形式化為：
現(xiàn)在，我們要試著把后一個「sorry」填上。
在 PFR github 倉庫的本地副本中，陶哲軒用編輯器（Visual Studio Code，擴展名為 lean4）打開了相關的 Lean 文件，并導航到「rdist_nonneg」的「sorry」處。
隨附的「Lean 信息視圖」就會顯示 Lean 證明的當前狀態(tài)：
在底部，可以看到我們需要證明的目標。
接下來，在證明這個說法時，需要運用一系列「戰(zhàn)術」來改變目標和 / 或假設。
第一步是加入應用 Lemma 3.11 所需的因子 2。
現(xiàn)在，我們有了兩個目標（和兩個「sorry」）：一個是證明 0≤2d [X;Y] 等價于 0≤d [X;Y]；另一個是證明 0≤2d [X;Y]。
在填上第一個「sorry」之后的狀態(tài)如下（刪去了一些無關的假設）：
這里可以使用一種非常方便的「linarith」策略，它能解決任何可以通過現(xiàn)有假設的線性運算得出的目標：
成功之后可以看到，狀態(tài)報告顯示這個分支已經(jīng)沒有需要證明的目標了。所以，我們繼續(xù)剩下的「sorry」，也就是證明 0≤2d [X;Y]：
在這里，我們將嘗試引用 Lemma 3.11。為此，陶哲軒添加了幾行代碼：
于是，我們又有了兩個子目標，一個是證明約束
（可以稱之為「h」），另一個是就從 h 推導出前一個目標 0≤2d [X;Y]。
對于第一個目標，需要調(diào)用正在編碼 Lemma 3.11 的「diff_ent_le_rdist」引理。
其中一種方法是嘗試使用「exact? 」策略，它會自動搜索，看目標是否可以立即從現(xiàn)有的引理中推導出來：
于是，陶哲軒點擊了建議的代碼（系統(tǒng)會自動將其粘貼到正確的位置）。結果成功了，只留下最后的「sorry」：
這里，陶哲軒通用使用了「exact?」策略，并按照它的建議建立匹配了邊界
：
在補全最后一個「sorry」時，陶哲軒再一次嘗試了「exact?」，想知道如何把 h 和 h' 結合起來才能達到預期目標，結果成功了！
可以看到，所有的下劃線都消失了。也就是說，Lean 已將其視為有效證明。
通過省略幾個中間步驟，我們可以將這個證明壓縮得相當緊湊：
現(xiàn)在證明完成了！
我們最后得到的，基本就是一個「單線證明」，考慮到 Lemma 3.11 和 Lemma 3.13 是如此接近，這也是合情合理的。
然后，陶哲軒將所有內(nèi)容推送回 Github 主版本庫。
Blueprint 的重建需要相當長的時間（約半小時），依賴關系圖現(xiàn)在以綠色顯示 「ruzsa-nonneg」：
因此可以說，PFR 的形式化更接近完成了。
不過，雖然「ruzsa-nonneg」現(xiàn)在被涂成綠色，但還沒有這個結果的完整證據(jù)，因為它所依賴的引理「ruzsa-diff」不是綠色的。
從這一點上看，證明仍然是局部完成的。
陶哲軒表示，希望在未來的某個時候，前身結果也能被證明，那時，就可以說 PFR 猜想的結果，得到了完全的證明。
參考資料：
https://news.ycombinator.com/item?id=38528582
https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/
本文來自微信公眾號：新智元 （ID：AI_era）
廣告聲明：文內(nèi)含有的對外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時間，結果僅供參考，IT之家所有文章均包含本聲明。