3天后，陶哲軒YouTube視頻二更來(lái)了。

上一次，他使用GitHub Copilot（基于GPT-4），成功在33分鐘內(nèi)完成一頁(yè)非形式化證明。

這次，他嘗試了一種更短、更概念化的證明版本，并測(cè)試Claude、o4-mini能否基于之前的非形式和形式證明，生成類似的形式化代碼。

實(shí)驗(yàn)的核心是，在Lean中形式化同一個(gè)代數(shù)蘊(yùn)含的證明。

此外，他還發(fā)文深入剖析了，自動(dòng)化工具不同尺度上的效率表現(xiàn)，以及自動(dòng)化與人工干預(yù)之間的微妙平衡。

Claude 20分完成，o4-mini棄題

最新實(shí)驗(yàn)中，陶哲軒圍繞一個(gè)代數(shù)蘊(yùn)含展開(kāi)（algebraic implication）：證明方程1689蘊(yùn)含方程2。

錄制前，他已進(jìn)行了一次測(cè)試。

這里直接在Claude/o4-mini中粘貼prompt，然后附上非形式證明、形式證明、方程三個(gè)附件。

接下來(lái)，一起看看這兩個(gè)模型具體表現(xiàn)如何？

Claude

實(shí)驗(yàn)中，Claude整體表現(xiàn)出色，能夠快速將非形式證明的單行，轉(zhuǎn)化為看似合理的Lean代碼。

它生成了與之前形式化證明結(jié)構(gòu)相似的代碼，并成功定義了關(guān)鍵的冪函數(shù)。

然而，陶哲軒創(chuàng)建一個(gè)新文件，在Claude編譯過(guò)程中，卻發(fā)現(xiàn)錯(cuò)誤——它假設(shè)從自然數(shù)1開(kāi)始，而Lean中的自然數(shù)從0開(kāi)始。

另外，Claude未能正確處理方程的對(duì)稱性，比如x=(y·x)·z，導(dǎo)致了證明邏輯出現(xiàn)偏差。

盡管單行代碼生成高效，但缺乏對(duì)整體結(jié)構(gòu)的理解，使得錯(cuò)誤診斷和修復(fù)變得困難。

通過(guò)人工干預(yù)，陶哲軒修復(fù)了這些問(wèn)題，最終在20分鐘內(nèi)完成形式化。

o4-mini

相比之下，o4-mini表現(xiàn)得更為謹(jǐn)慎。

與Claude類似，o4-mini一上來(lái)也創(chuàng)建了一個(gè)冪函數(shù)，卻勝過(guò)前者。

它正確識(shí)別了冪函數(shù)定義中的問(wèn)題，magmas中沒(méi)有單位元1，因此不能簡(jiǎn)單假設(shè)0=>x設(shè)置為等于1。

然而，o4-mini在關(guān)鍵時(shí)刻卻選擇了「放棄」，僅生成了部分證明代碼，并在修復(fù)步驟中輸出「抱歉」。

最終，o4-mini未能完成形式化證明。

陶哲軒表示，它的謹(jǐn)慎策略雖避免了嚴(yán)重錯(cuò)誤，但也限制了其在復(fù)雜任務(wù)中的實(shí)用性。

有趣的是，o4-mini和Claude同樣遇到了類似對(duì)稱性問(wèn)題，表明LLM在處理數(shù)學(xué)邏輯的細(xì)微差別時(shí)，存在共同的局限。

總之，整個(gè)實(shí)驗(yàn)?zāi)繕?biāo)看似簡(jiǎn)單，即讓AI工具將人類可讀的證明轉(zhuǎn)化為L(zhǎng)ean代碼，并在證明助手中成功編譯。

然而，陶哲軒的實(shí)驗(yàn)揭示了自動(dòng)化的復(fù)雜性，尤其是在效率和正確性之間的平衡。

100%過(guò)度自動(dòng)化，毀掉數(shù)學(xué)未來(lái)？

在長(zhǎng)達(dá)一周的自動(dòng)形式化實(shí)驗(yàn)中，陶哲軒得出了一個(gè)教訓(xùn)——

即使純粹專注于效率，僅接受在證明助手中實(shí)際編譯并產(chǎn)生預(yù)期結(jié)果的形式化，衡量效率的尺度現(xiàn)在也產(chǎn)生了顯著差異。

在形式化數(shù)學(xué)證明過(guò)程中，效率可以從以下四個(gè)不同尺度衡量。

1. 單形式化：加快證明中任意一行的形式化

2. 單一引理形式化：加快形式化證明中的任一引理

3. 單一證明形式化：加快形式化定理的任一證明

4. 「整個(gè)教科書」形式化：加快形式化整個(gè)教科書的成果

每個(gè)尺度看似都在指向同一個(gè)目標(biāo)：更快地完成形式化。然而，實(shí)際操作中，這些尺度的優(yōu)化策略可能互相沖突。

陶哲軒以自己最近的實(shí)驗(yàn)為例，嘗試用一些自動(dòng)化工具，加速形式化過(guò)程。

我意識(shí)到，許多當(dāng)前的自動(dòng)化工具可以在其中一個(gè)尺度上加速形式化，但出乎意料的是，過(guò)度依賴此類工具可能會(huì)削弱在其他尺度上形式化的能力。

比如，依賴類型匹配工具canonical在「單行形式化」（尺度1）的任務(wù)中，表現(xiàn)出色。

它能快速解析，并生成正確的代碼，在此過(guò)程中，陶哲軒幾乎無(wú)需手動(dòng)干預(yù)。

然而，當(dāng)過(guò)于依賴canonical，盲目接受它對(duì)某一步的解析，并迅速進(jìn)入下一步時(shí)，他發(fā)現(xiàn)自己逐漸失去了對(duì)證明整體結(jié)構(gòu)的把握。

這導(dǎo)致了，在「引理形式化」（尺度2）上，診斷和修復(fù)錯(cuò)誤變得更加困難，因?yàn)榈搅舜丝蹋照苘帉?duì)證明步驟之間的聯(lián)系缺乏深入的理解。

有趣的是，修復(fù)這些錯(cuò)誤的過(guò)程，卻讓陶哲軒本人受益匪淺。

通過(guò)手動(dòng)檢查和調(diào)整，他逐漸理解了引理之間的作用，這反過(guò)來(lái)提升了其解決「單一證明形式化」（尺度3）任務(wù)的能力。

這種「意外收獲」讓他意識(shí)到，完全依賴自動(dòng)化工具，可能會(huì)讓自己錯(cuò)過(guò)對(duì)證明結(jié)構(gòu)的深刻洞察，而這些這些洞察在更大尺度上至關(guān)重要。

陶哲軒認(rèn)為結(jié)論是，「最優(yōu)的自動(dòng)化水平并不是100%，而是介于0%和100%之間的某個(gè)值」。

從每個(gè)尺度上來(lái)說(shuō)，自動(dòng)化工具應(yīng)該被用來(lái)減少重復(fù)性的繁瑣工作，但同時(shí)必須保留足夠的人為干預(yù)，以審查和修復(fù)局部問(wèn)題，從加深人類對(duì)所有尺度任務(wù)結(jié)構(gòu)的理解。

更廣義地看，如果我們100%依賴自動(dòng)化工具解決所有任務(wù)，可能會(huì)失去對(duì)任務(wù)空間的熟悉度。

在面對(duì)中等，甚至高難度任務(wù)時(shí)，自動(dòng)化工具可靠性下降，我們卻可能因缺乏經(jīng)驗(yàn)而束手無(wú)策。

值得警醒的是，過(guò)度聚焦于單一尺度的效率優(yōu)化，可能會(huì)違背數(shù)學(xué)形式化的長(zhǎng)遠(yuǎn)目標(biāo)。

其終極目標(biāo)，不僅是生成在證明助手中編譯的代碼，更是要?jiǎng)?chuàng)造一個(gè)靈活、可用、不斷演變且富有啟發(fā)性的形式化數(shù)學(xué)語(yǔ)料庫(kù)。