陶哲軒油管首戰：33分鐘，AI速證「人類需要寫滿一頁紙」的證明

白交 一水 發自 凹非寺

量子位 | 公眾號 QbitAI

快來圍觀，陶哲軒當影片博主了。

第一個產出就很炸裂：人類需要寫滿一頁紙的證明，結果借助AI 33分鐘就搞掂了？！

整個過程看起來一氣嗬成，還是全程「盲證」不用過腦子那種。

對於這一操作，網民們驚呆：這具有足夠的歷史意義。

在沒有明顯引導、宣傳之下，他的訂閱數一天時間已經有900+，觀看數超兩千，目前仍然在高速增長中。

大家趕在爆火之前留言：

今天我們相聚在這裏，就是為了見證偉大數學頻道的誕生。

具體來看看是如何做到？

33分鐘盲證定理

陶哲軒這次選取了泛代數中的一個命題，即證明Magma方程E1689蘊含E2。

方程具體是什麼不重要，我們只需要瞭解，即使是方程理論項目的合作者Bruno Le Floch，也足足人工花了一頁紙才完成證明。

而用上AI後，整個證明過程僅用時33分鐘：

具體而言，陶哲軒嘗試完全基於Bruno Le Floch的草稿，逐行進行形式化。

他將草稿拆分為微小邏輯單元，交由GitHub Copilot生成代碼骨架，再以Lean的canonical策略匹配填補細節，過程中也涉及部分手動補全。

最終，整個形式化證明能夠在Lean中通過驗證。

不僅時間大大縮短了，更重要的是滿足了「人類可讀性」。

要知道Bruno Le Floch最初挑戰該問題時，曾在論文中宣稱E1689-E2的所有已知證明都依賴計算機輔助。

直到後來他使用prover9 ATP（自動定理證明器）給出了一個更具可讀性的人類版本，所以才對之前的想法產生動搖：

它是否仍然可以被認為是計算機輔助的，我不確定。

針對這一疑惑，陶哲軒提議今後可以在論文中明確說明，雖然最初的證明是由計算機生成的，但在項目進行過程中，研究者們成功地將其轉化為一個人類可讀的證明。

並且為了實際驗證AI能在多大程度上開啟自動化形式證明，陶哲軒就此開啟了本次YouTube首戰。

通過幾次親自嘗試，陶哲軒得出了如下結論：

這種半自動化的方法適用於那些技術性強、概念性弱的論證，即那些主要關注細節準確性而非整體概念理解的證明。

並且他再一次強調，AI輔助證明能夠把數學家從一些相對不重要的繁瑣事務中解放出來，「讓AI去做一些它擅長的事」。

在他看來，儘管最終的結果「並不優雅」，但它體現了AI輔助證明的巨大潛力。

最後需要說明一下，陶哲軒並非一次就成功了。

據他在影片中透露，前兩次的證明過程都出現了一些「bug」——

第一次拿到的代碼才到第5行他就有點看不懂了，所以選擇了重開；第二次雖然完成了所有證明（用時48分鐘），但由於是新人博主不太熟悉錄屏設備，導致屏幕分享失敗，因此又只能重來。

數學證明助手迎來2.0版本

此外，還有他開發的數學證明助手迎來2.0版本升級。

根據介紹，這是一個用Python開發的輕量級證明助手，其功能遠遜於Lean、Isabelle或Rocq等完整證明助手，但（希望）它能夠輕鬆用於證明一些簡短而繁瑣的任務。

一個具體的目標是，為漸近分析提供支持。

兩週前，在大模型的幫助之下，他花了四個小時編程得到了這麼一個概念驗證工具。

結果不到兩週，這個工具就迎來了全面改進——

首先，將其改造成一個基本的證明助手，使其能夠處理一些命題邏輯；其次，根據反饋，這個證明助手變得更為靈活（在幾個關鍵方面刻意模仿精簡證明助手）。

目前這個助手有兩種模式：假設模式和策略模式。其中策略模式作為預設模式，有點類似於Lean、Isabelle或Rocq裡面那樣式兒的策略模式。

目前策略列表主要分為四類：

• 命題策略（主要圍繞通過布爾運算操縱命題）

• 線性算術策略（依賴於線性規劃及其變體）

• 替代策略——用一個假設或目標替代另一個假設或目標的各種技術

• 簡化策略——利用其他可用假設來「簡化」假設或目標的方法

當然這些還不是全部，這個助手支持擴展，大家可以在裡面進行添加。

舉個例子。

如果x，y，z是正實數，且x<2y和y<3z+1，證明x<7z+2。

將它形式化就會變成：

>>> from main import *>>> p = linarith_exercise()Starting proof.  Current proof state:x: pos_realy: pos_realz: pos_realh1: x < 2*yh2: y < 3*z + 1|- x < 7*z + 2

證明助手接收到指令後，指導助手使用各種「策略」來簡化問題，直到問題得到解決。

那麼這個問題可以通過線性算術Linarith()求解。

>>> p.use(Linarith())Goal solved by linear arithmetic!Proof complete!

如果想要有詳細解釋，也是OK的：

>>> from main import *>>> p = linarith_exercise()Starting proof.  Current proof state:x: pos_realy: pos_realz: pos_realh1: x < 2*yh2: y < 3*z + 1|- x < 7*z + 2>>> p.use(Linarith(verbose=true))Checking feasibility of the following inequalities:1*z > 01*x + -7*z >= 21*y + -3*z < 11*y > 01*x > 01*x + -2*y < 0Infeasible by summing the following:1*z > 0 multiplied by 1/41*x + -7*z >= 2 multiplied by 1/41*y + -3*z < 1 multiplied by -1/21*x + -2*y < 0 multiplied by -1/4Goal solved by linear arithmetic!Proof complete!

可以看到，首先，它通過反證法進行論證，即採用否定x≥7z+2目標x<7z+2並將其添加到假設中。

然後，它將假設中所有不等式轉化為「線性規劃」形式，變量在左邊，常數在右邊。

最後，它使用精確線性規劃來尋找這些不等式的線性組合，從而導致荒謬的不等式，在這種情況下0<1。

解決完問題之後，還可以使用proof（）進行檢查。

有時候，遇到證明過程會涉及案例拆分的情況，那麼證明助手最終會呈現樹狀結構。

對於這個證明助手，陶哲軒表示：非常滿意，並且願意接受進一步的建議或貢獻新的功能。比如引入新的數據類型、公例和策略，或者貢獻一些有難度的例子。

此外還計劃開發用於估算符號函數的函數空間規範的工具。例如創建部署霍爾德不等式和索博列夫嵌入不等式等定理的策略。看起來sympy框架足夠靈活，可以為這類對象創建更多的對象類。

感興趣的旁友，可以前往去體驗下哦。

參考鏈接：

[1]https://mathstodon.xyz/@tao/114486537464033675

[2]https://www.youtube.com/watch?v=cyyR7j2ChCI

[3]https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean