陶哲軒聯手AI挑戰經典ε-δ極限！加法秒殺、乘法翻車
數學大師陶哲軒的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更像是你的「得力助手」，適合在你已經大致知道證明方向時，幫你快速搞定那些重復的、格式化的工作。
它是個超強的輔助工具，但證明的策略、方向和最終驗證，還是得靠人類自己來把控。
