快來(lái)圍觀(guān)，陶哲軒當(dāng)視頻博主了。

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

整個(gè)過(guò)程看起來(lái)一氣呵成，還是全程“盲證”不用過(guò)腦子那種。

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

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

大家趕在爆火之前留言：

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

具體來(lái)看看是如何做到？

33分鐘盲證定理

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

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

而用上AI后，整個(gè)證明過(guò)程僅用時(shí)33分鐘：

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

他將草稿拆分為微小邏輯單元，交由GitHub Copilot生成代碼骨架，再以L(fǎng)ean的canonical策略匹配填補(bǔ)細(xì)節(jié)，過(guò)程中也涉及部分手動(dòng)補(bǔ)全。

最終，整個(gè)形式化證明能夠在Lean中通過(guò)驗(yàn)證。

不僅時(shí)間大大縮短了，更重要的是滿(mǎn)足了“人類(lèi)可讀性”。

要知道Bruno Le Floch最初挑戰(zhàn)該問(wèn)題時(shí)，曾在論文中宣稱(chēng)E1689-E2的所有已知證明都依賴(lài)計(jì)算機(jī)輔助。

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

它是否仍然可以被認(rèn)為是計(jì)算機(jī)輔助的，我不確定。

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

并且為了實(shí)際驗(yàn)證AI能在多大程度上開(kāi)啟自動(dòng)化形式證明，陶哲軒就此開(kāi)啟了本次YouTube首秀。

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

這種半自動(dòng)化的方法適用于那些技術(shù)性強(qiáng)、概念性弱的論證，即那些主要關(guān)注細(xì)節(jié)準(zhǔn)確性而非整體概念理解的證明。

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

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

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

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

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

數(shù)學(xué)證明助手迎來(lái)2.0版本

此外，還有他開(kāi)發(fā)的數(shù)學(xué)證明助手迎來(lái)2.0版本升級(jí)。

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

一個(gè)具體的目標(biāo)是，為漸近分析提供支持。

兩周前，在大模型的幫助之下，他花了四個(gè)小時(shí)編程得到了這么一個(gè)概念驗(yàn)證工具。

結(jié)果不到兩周，這個(gè)工具就迎來(lái)了全面改進(jìn)——

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

目前這個(gè)助手有兩種模式：假設(shè)模式和策略模式。其中策略模式作為默認(rèn)模式，有點(diǎn)類(lèi)似于Lean、Isabelle或Rocq里面那樣式兒的策略模式。

目前策略列表主要分為四類(lèi)：

• 命題策略（主要圍繞通過(guò)布爾運(yùn)算操縱命題）
• 線(xiàn)性算術(shù)策略（依賴(lài)于線(xiàn)性規(guī)劃及其變體）
• 替代策略——用一個(gè)假設(shè)或目標(biāo)替代另一個(gè)假設(shè)或目標(biāo)的各種技術(shù)
• 簡(jiǎn)化策略——利用其他可用假設(shè)來(lái)“簡(jiǎn)化”假設(shè)或目標(biāo)的方法

當(dāng)然這些還不是全部，這個(gè)助手支持?jǐn)U展，大家可以在里面進(jìn)行添加。

舉個(gè)例子。

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

將它形式化就會(huì)變成：

>>> 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

證明助手接收到指令后，指導(dǎo)助手使用各種“策略”來(lái)簡(jiǎn)化問(wèn)題，直到問(wèn)題得到解決。

那么這個(gè)問(wèn)題可以通過(guò)線(xiàn)性算術(shù)Linarith()求解。

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

如果想要有詳細(xì)解釋?zhuān)彩荗K的：

>>> 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!

可以看到，首先，它通過(guò)反證法進(jìn)行論證，即采用否定x≥7z+2目標(biāo)x<7z+2并將其添加到假設(shè)中。

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

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

解決完問(wèn)題之后，還可以使用proof（）進(jìn)行檢查。

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

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

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

感興趣的旁友，可以前往去體驗(yàn)下哦。