新智元報道
新智元報道
編輯：犀牛
【新智元導讀】數學大師陶哲軒的第三支Lean 4自動化數學證明影片來了！他攜手GitHub Copilot挑戰分析學經典的「ε-δ」極限問題：加法定理Copilot揮灑自如，減法開始卡殼，乘法更是全面失控。Copilot究竟是神助攻還是添亂？
數學大師陶哲軒的AI新實驗來了！
這次是Lean 4自動化數學證明的第三支影片。
主要看看GitHub Copilot在處理分析學經典的「ε-δ」問題（描述函式極限的經典方法）時，效果究竟如何。
之前，陶哲軒上傳了兩支這個系列的影片。
加上此次的一共3支影片，陶哲軒的油管頻道已經有1.7萬位訂閱者了。
看來，他作為菲爾茲獎得主、當代最傑出數學家之一的影響力的確毋庸置疑。
陶哲軒在此次定理形式化演示中發現，GitHub Copilot在幫助新手入門和處理基礎任務時表現得相當不錯。
它能幫助使用者快速上手Lean語言（一種互動式定理證明工具），提供語法提示，並智慧補全基本定義和宣告。
在比較簡單的證明，比如函式極限的和定理中，Copilot還能準確預測證明結構和關鍵步驟，表現得就像個得力助手一樣。
但當證明變得複雜時，Copilot的短板就暴露出來了。
比如在處理函式極限的差和積定理時，它在複雜的代數推導、尋找合適的數學引理（比如與絕對值相關的引理）等方面顯得力不從心。
Copilot有時還會出現「幻覺」，生成壓根不存在的策略，或者犯一些低階錯誤，導致證明過程亂成一團。
這時，陶哲軒不得不親自出馬，修正錯誤，甚至完全接管證明。
「人機協作」的證明過程
形式化數學的目標是用計算機能完全看懂的精確語言，把數學概念和證明寫出來，再用定理證明工具（比如影片裡提到的Lean）來一步步檢查推理是否靠譜。
這就像把數學證明翻譯成一種特別嚴謹的程式語言。
第三彈的影片裡，陶哲軒從一個經典的分析學概念入手：函式的極限。
用Lean把這個定義寫出來，對新手來說真不是件容易事兒。不過，GitHub Copilot就像個貼心助手，派上了大用場。
陶哲軒剛敲下「定義一個謂詞limit f x₀ l」，Copilot就立刻get到他想表達的是「ε-δ」極限定義，秒秒鐘生成了對應的Lean程式碼。
雖然陶哲軒根據自己的習慣稍作調整，但Copilot的智慧補全明顯讓整個過程快了不少。
「和的極限」——小試牛刀
接下來，陶哲軒挑戰了一個更復雜的定理：如果函式f(x)的極限是L，g(x)的極限是M，那麼f(x)+g(x)的極限就是L+M。
Copilot又秀了一把操作。它不僅幫陶哲軒寫出了定理的Lean宣告，還開始「猜」證明的步驟，建議引入假設，提取出ε和δ這些關鍵變數。
Copilot嘗試用Lean的calc塊整理不等式鏈，還試著用simp簡化表示式。
但這裡它開始出小差錯，比如搞亂了絕對值的位置，或者在代數推導時顯得不夠「機智」。
陶哲軒不得不出手，比如他提醒Copilot用「ε/2」技巧。Copilot雖然一開始沒完全跟上，但調整後成功融入了這個思路。
最終，經過一番人機配合，這個「和的極限」定理在Lean裡被順利證明透過。
陶哲軒覺得，Copilot幹了大部分活，互動體驗也很不錯。
「差的極限」——AI有點懵
有了「和的極限」的經驗，陶哲軒以為「差的極限」會同樣順利。這個定理是說，如果f(x)的極限是L，g(x)的極限是M，那麼f(x)-g(x)的極限是L-M。
Copilot似乎也信心滿滿，直接套用了「和的極限」的證明套路，甚至用上了上述的「ε/2」的技巧。
但過程中，Copilot還是卡殼了，甚至還「腦補」了一個Lean里根本不存在的策略（叫什麼sub subanc）。
面對Copilot的「胡思亂想」，陶哲軒試圖給予提示，但Copilot還是搞不懂。
陶哲軒意識到，這些代數變換對人類來說簡單，但在Lean裡需要呼叫特定的數學引理來支撐每一步。最終，陶哲軒只能親自動手完成這些代數推導。
這一關讓陶哲軒看到，Copilot雖然能模仿證明的大框架，但在需要特定引理或複雜代數操作時，容易掉鏈子。
他給Copilot這一關的表現打了個B+：幫了不少忙，但關鍵時刻還是得靠人類引導甚至接管。
「積的極限」——徹底亂套
最難的來了：如果f(x)的極限是L，g(x)的極限是M，那麼f(x)·g(x)的極限是L·M。
這個證明比加減法複雜多了，尤其在控制誤差（ε）時，堪稱噩夢。
Copilot嘗試沿用標準套路，加中間項、三角不等式。
但問題來了，Lean裡處理絕對值乘積或求和，需要非常具體的引理，比如把|ab|變成|a||b|得用abs_mul，|a+b|≤|a|+|b|得用abs_add。
Copilot在找這些引理時頻頻出錯，甚至想用一些通用的策略（比如線性算術），卻因為有乘法和絕對值而行不通。
更麻煩的是，為了讓誤差控制在ε內，一開始得精心設計f(x)和g(x)的誤差引數。這些引數選擇和邊界估計對Copilot來說有點太難了，它試了些引數，但證明中發現行不通，甚至還差點弄出除以零的錯誤。
陶哲軒在這階段花了大量時間「救火」，不斷調整Copilot的嘗試，尋找正確的引理，甚至回去改最初的誤差引數。
整個過程亂成一團，儘管Lean系統改引數相對方便（改了讓系統重查就行），但得對證明結構有清晰理解才知道怎麼改。
最終，經過艱苦努力和大量人工干預，陶哲軒完成了「積的極限」證明。
他總結說，一旦證明覆雜到一定程度，Copilot就變得「不怎麼靠譜」了。
證明的完整程式碼在GitHub中：
import Mathlib/- In this file we are going to give some "epsilon-delta" proofs of facts about limits of functions on the real line. -//- First, we give the epsilon-delta definition of what it means for a function f : R -> R to converge to a limit L at a value x_0. -/def limit (f : ℝ → ℝ) (L : ℝ) (x_0 : ℝ) : Prop := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x_0| < δ → |f x - L| < ε/-- First we show that if a function f converges to a limit L at x_0, and a function g converges to a limit M at x_0, then f+g converge to L+M at x_0. -/lemma limit_add (f g : ℝ → ℝ) (L M : ℝ) (x_0 : ℝ) :limit f L x_0 → limit g M x_0 → limit (fun x => f x + g x) (L + M) x_0 := by intro h1 h2 ε hε -- Use ε/2 for each function have hε2 : 0 < ε / 2 := half_pos hε rcases h1 (ε / 2) hε2 with ⟨δ₁, hδ₁, h1'⟩ rcases h2 (ε / 2) hε2 with ⟨δ₂, hδ₂, h2'⟩let δ := min δ₁ δ₂ use δ constructor · exact lt_min hδ₁ hδ₂ intro x hx...程式碼地址：https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/limits.lean
有意思的是，大部分觀眾都覺得影片做得很棒，不過不少網友都建議陶哲軒換個新麥克風，以消除迴音。
AI只是副駕駛
在影片的最後，陶哲軒總結道：當證明過程變得複雜時，不如回到最傳統的「人腦」方式——拿支筆在紙上把證明的思路和關鍵步驟理得清清楚楚，再去證明器裡一步步形式化。
Copilot更像是你的「得力助手」，適合在你已經大致知道證明方向時，幫你快速搞定那些重複的、格式化的工作。
它是個超強的輔助工具，但證明的策略、方向和最終驗證，還是得靠人類自己來把控。
參考資料：
https://www.youtube.com/watch?v=c1ixXMtmfS8
