快來圍觀，陶哲軒當視頻博主了。

第一個產(chǎn)出就很炸裂：人類需要寫滿一頁紙的證明，結(jié)果借助AI 33分鐘就搞定了？！

整個過程看起來一氣呵成，還是全程“盲證”不用過腦子那種。

對于這一操作，網(wǎng)友們驚呆：這具有足夠的歷史意義。

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

大家趕在爆火之前留言：

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

具體來看看是如何做到？

33分鐘盲證定理

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

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

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

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

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

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

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

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

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

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

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

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

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

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

并且他再一次強調(diào)，AI輔助證明能夠把數(shù)學家從一些相對不重要的繁瑣事務中解放出來，“讓AI去做一些它擅長的事”。

在他看來，盡管最終的結(jié)果“并不優(yōu)雅”，但它體現(xiàn)了AI輔助證明的巨大潛力。

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

據(jù)他在視頻中透露，前兩次的證明過程都出現(xiàn)了一些“bug”——

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

數(shù)學證明助手迎來2.0版本

此外，還有他開發(fā)的數(shù)學證明助手迎來2.0版本升級。

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

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

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

結(jié)果不到兩周，這個工具就迎來了全面改進——

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

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

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

• 命題策略（主要圍繞通過布爾運算操縱命題）
• 線性算術策略（依賴于線性規(guī)劃及其變體）
• 替代策略——用一個假設或目標替代另一個假設或目標的各種技術
• 簡化策略——利用其他可用假設來“簡化”假設或目標的方法

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

舉個例子。

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

將它形式化就會變成：

>>> from main import *
>>> p = linarith_exercise()
Starting proof.  Current proof state:
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: 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_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3*z + 1
|- x < 7*z + 2
>>> p.use(Linarith(verbose=true))
Checking feasibility of the following inequalities:
1*z > 0
1*x + -7*z >= 2
1*y + -3*z < 1
1*y > 0
1*x > 0
1*x + -2*y < 0
Infeasible by summing the following:
1*z > 0 multiplied by 1/4
1*x + -7*z >= 2 multiplied by 1/4
1*y + -3*z < 1 multiplied by -1/2
1*x + -2*y < 0 multiplied by -1/4
Goal solved by linear arithmetic!
Proof complete!

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

然后，它將假設中所有不等式轉(zhuǎn)化為“線性規(guī)劃”形式，變量在左邊，常數(shù)在右邊。

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

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

有時候，遇到證明過程會涉及案例拆分的情況，那么證明助手最終會呈現(xiàn)樹狀結(jié)構(gòu)。

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

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

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