3天后，陶哲軒YouTube視頻二更來了。

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

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

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

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

Claude 20分完成，o4-mini棄題

最新實驗中，陶哲軒圍繞一個代數(shù)蘊含展開（algebraic implication）：證明方程1689蘊含方程2。

錄制前，他已進行了一次測試。

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

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

Claude

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

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

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

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

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

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

o4-mini

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

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

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

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

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

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

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

總之，整個實驗?zāi)繕丝此坪唵?，即讓AI工具將人類可讀的證明轉(zhuǎn)化為Lean代碼，并在證明助手中成功編譯。

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

100%過度自動化，毀掉數(shù)學(xué)未來？

在長達一周的自動形式化實驗中，陶哲軒得出了一個教訓(xùn)——

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

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

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

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

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

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

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

陶哲軒以自己最近的實驗為例，嘗試用一些自動化工具，加速形式化過程。

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

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

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

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

這導(dǎo)致了，在「引理形式化」（尺度2）上，診斷和修復(fù)錯誤變得更加困難，因為到了此刻，陶哲軒對證明步驟之間的聯(lián)系缺乏深入的理解。

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

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

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

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

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

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

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

值得警醒的是，過度聚焦于單一尺度的效率優(yōu)化，可能會違背數(shù)學(xué)形式化的長遠目標。

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