數(shù)學(xué)大師陶哲軒的AI新實(shí)驗(yàn)來(lái)了！

這次是Lean 4自動(dòng)化數(shù)學(xué)證明的第三支視頻。

主要看看GitHub Copilot在處理分析學(xué)經(jīng)典的「ε-δ」問(wèn)題（描述函數(shù)極限的經(jīng)典方法）時(shí)，效果究竟如何。

之前，陶哲軒上傳了兩支這個(gè)系列的視頻。

加上此次的一共3支視頻，陶哲軒的油管頻道已經(jīng)有1.7萬(wàn)位訂閱者了。

看來(lái)，他作為菲爾茲獎(jiǎng)得主、當(dāng)代最杰出數(shù)學(xué)家之一的影響力的確毋庸置疑。

陶哲軒在此次定理形式化演示中發(fā)現(xiàn)，GitHub Copilot在幫助新手入門和處理基礎(chǔ)任務(wù)時(shí)表現(xiàn)得相當(dāng)不錯(cuò)。

它能幫助用戶快速上手Lean語(yǔ)言（一種交互式定理證明工具），提供語(yǔ)法提示，并智能補(bǔ)全基本定義和聲明。

在比較簡(jiǎn)單的證明，比如函數(shù)極限的和定理中，Copilot還能準(zhǔn)確預(yù)測(cè)證明結(jié)構(gòu)和關(guān)鍵步驟，表現(xiàn)得就像個(gè)得力助手一樣。

但當(dāng)證明變得復(fù)雜時(shí)，Copilot的短板就暴露出來(lái)了。

比如在處理函數(shù)極限的差和積定理時(shí)，它在復(fù)雜的代數(shù)推導(dǎo)、尋找合適的數(shù)學(xué)引理（比如與絕對(duì)值相關(guān)的引理）等方面顯得力不從心。

Copilot有時(shí)還會(huì)出現(xiàn)「幻覺(jué)」，生成壓根不存在的策略，或者犯一些低級(jí)錯(cuò)誤，導(dǎo)致證明過(guò)程亂成一團(tuán)。

這時(shí)，陶哲軒不得不親自出馬，修正錯(cuò)誤，甚至完全接管證明。

「人機(jī)協(xié)作」的證明過(guò)程

形式化數(shù)學(xué)的目標(biāo)是用計(jì)算機(jī)能完全看懂的精確語(yǔ)言，把數(shù)學(xué)概念和證明寫出來(lái)，再用定理證明工具（比如視頻里提到的Lean）來(lái)一步步檢查推理是否靠譜。

這就像把數(shù)學(xué)證明翻譯成一種特別嚴(yán)謹(jǐn)?shù)木幊陶Z(yǔ)言。

第三彈的視頻里，陶哲軒從一個(gè)經(jīng)典的分析學(xué)概念入手：函數(shù)的極限。

用Lean把這個(gè)定義寫出來(lái)，對(duì)新手來(lái)說(shuō)真不是件容易事兒。不過(guò)，GitHub Copilot就像個(gè)貼心助手，派上了大用場(chǎng)。

陶哲軒剛敲下「定義一個(gè)謂詞limit f x? l」，Copilot就立刻get到他想表達(dá)的是「ε-δ」極限定義，秒秒鐘生成了對(duì)應(yīng)的Lean代碼。

雖然陶哲軒根據(jù)自己的習(xí)慣稍作調(diào)整，但Copilot的智能補(bǔ)全明顯讓整個(gè)過(guò)程快了不少。

「和的極限」——小試牛刀

接下來(lái)，陶哲軒挑戰(zhàn)了一個(gè)更復(fù)雜的定理：如果函數(shù)f(x)的極限是L，g(x)的極限是M，那么f(x)+g(x)的極限就是L+M。

Copilot又秀了一把操作。它不僅幫陶哲軒寫出了定理的Lean聲明，還開(kāi)始「猜」證明的步驟，建議引入假設(shè)，提取出ε和δ這些關(guān)鍵變量。

Copilot嘗試用Lean的calc塊整理不等式鏈，還試著用simp簡(jiǎn)化表達(dá)式。

但這里它開(kāi)始出小差錯(cuò)，比如搞亂了絕對(duì)值的位置，或者在代數(shù)推導(dǎo)時(shí)顯得不夠「機(jī)智」。

陶哲軒不得不出手，比如他提醒Copilot用「ε/2」技巧。Copilot雖然一開(kāi)始沒(méi)完全跟上，但調(diào)整后成功融入了這個(gè)思路。

最終，經(jīng)過(guò)一番人機(jī)配合，這個(gè)「和的極限」定理在Lean里被順利證明通過(guò)。

陶哲軒覺(jué)得，Copilot干了大部分活，互動(dòng)體驗(yàn)也很不錯(cuò)。

「差的極限」——AI有點(diǎn)懵

有了「和的極限」的經(jīng)驗(yàn)，陶哲軒以為「差的極限」會(huì)同樣順利。這個(gè)定理是說(shuō)，如果f(x)的極限是L，g(x)的極限是M，那么f(x)-g(x)的極限是L-M。

Copilot似乎也信心滿滿，直接套用了「和的極限」的證明套路，甚至用上了上述的「ε/2」的技巧。

但過(guò)程中，Copilot還是卡殼了，甚至還「腦補(bǔ)」了一個(gè)Lean里根本不存在的策略（叫什么sub subanc）。

面對(duì)Copilot的「胡思亂想」，陶哲軒試圖給予提示，但Copilot還是搞不懂。

陶哲軒意識(shí)到，這些代數(shù)變換對(duì)人類來(lái)說(shuō)簡(jiǎn)單，但在Lean里需要調(diào)用特定的數(shù)學(xué)引理來(lái)支撐每一步。最終，陶哲軒只能親自動(dòng)手完成這些代數(shù)推導(dǎo)。

這一關(guān)讓陶哲軒看到，Copilot雖然能模仿證明的大框架，但在需要特定引理或復(fù)雜代數(shù)操作時(shí)，容易掉鏈子。

他給Copilot這一關(guān)的表現(xiàn)打了個(gè)B+：幫了不少忙，但關(guān)鍵時(shí)刻還是得靠人類引導(dǎo)甚至接管。

「積的極限」——徹底亂套

最難的來(lái)了：如果f(x)的極限是L，g(x)的極限是M，那么f(x)·g(x)的極限是L·M。

這個(gè)證明比加減法復(fù)雜多了，尤其在控制誤差（ε）時(shí)，堪稱噩夢(mèng)。

Copilot嘗試沿用標(biāo)準(zhǔn)套路，加中間項(xiàng)、三角不等式。

但問(wèn)題來(lái)了，Lean里處理絕對(duì)值乘積或求和，需要非常具體的引理，比如把|ab|變成|a||b|得用abs_mul，|a+b|≤|a|+|b|得用abs_add。

Copilot在找這些引理時(shí)頻頻出錯(cuò)，甚至想用一些通用的策略（比如線性算術(shù)），卻因?yàn)橛谐朔ê徒^對(duì)值而行不通。

更麻煩的是，為了讓誤差控制在ε內(nèi)，一開(kāi)始得精心設(shè)計(jì)f(x)和g(x)的誤差參數(shù)。這些參數(shù)選擇和邊界估計(jì)對(duì)Copilot來(lái)說(shuō)有點(diǎn)太難了，它試了些參數(shù)，但證明中發(fā)現(xiàn)行不通，甚至還差點(diǎn)弄出除以零的錯(cuò)誤。

陶哲軒在這階段花了大量時(shí)間「救火」，不斷調(diào)整Copilot的嘗試，尋找正確的引理，甚至回去改最初的誤差參數(shù)。

整個(gè)過(guò)程亂成一團(tuán)，盡管Lean系統(tǒng)改參數(shù)相對(duì)方便（改了讓系統(tǒng)重查就行），但得對(duì)證明結(jié)構(gòu)有清晰理解才知道怎么改。

最終，經(jīng)過(guò)艱苦努力和大量人工干預(yù)，陶哲軒完成了「積的極限」證明。

他總結(jié)說(shuō)，一旦證明復(fù)雜到一定程度，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

有意思的是，大部分觀眾都覺(jué)得視頻做得很棒，不過(guò)不少網(wǎng)友都建議陶哲軒換個(gè)新麥克風(fēng)，以消除回音。

AI只是副駕駛

在視頻的最后，陶哲軒總結(jié)道：當(dāng)證明過(guò)程變得復(fù)雜時(shí)，不如回到最傳統(tǒng)的「人腦」方式——拿支筆在紙上把證明的思路和關(guān)鍵步驟理得清清楚楚，再去證明器里一步步形式化。

Copilot更像是你的「得力助手」，適合在你已經(jīng)大致知道證明方向時(shí)，幫你快速搞定那些重復(fù)的、格式化的工作。

它是個(gè)超強(qiáng)的輔助工具，但證明的策略、方向和最終驗(yàn)證，還是得靠人類自己來(lái)把控。