新智元報道

編輯：犀牛

【新智元導讀】數學大師陶哲軒的第三支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