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