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

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

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

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

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

Claude 20分完成，o4-mini棄題

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

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

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

接下來，一起看看這兩個模型具體表現如何？

Claude

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

它生成了與之前形式化證明結構相似的代碼，并成功定義了關鍵的冪函數。

然而，陶哲軒創建一個新文件，在Claude編譯過程中，卻發現錯誤——它假設從自然數1開始，而Lean中的自然數從0開始。

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

盡管單行代碼生成高效，但缺乏對整體結構的理解，使得錯誤診斷和修復變得困難。

通過人工干預，陶哲軒修復了這些問題，最終在20分鐘內完成形式化。

o4-mini

相比之下，o4-mini表現得更為謹慎。

與Claude類似，o4-mini一上來也創建了一個冪函數，卻勝過前者。

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

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

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

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

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

總之，整個實驗目標看似簡單，即讓AI工具將人類可讀的證明轉化為Lean代碼，并在證明助手中成功編譯。

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

100%過度自動化，毀掉數學未來？

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

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

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

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

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

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

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

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

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

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

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

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

然而，當過于依賴canonical，盲目接受它對某一步的解析，并迅速進入下一步時，他發現自己逐漸失去了對證明整體結構的把握。

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

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

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

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

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

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

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

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

值得警醒的是，過度聚焦于單一尺度的效率優化，可能會違背數學形式化的長遠目標。

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