視頻新人博主陶哲軒又更新了！這次是“喂飯級”AI教程——

手把手演示如何只用GitHub Copilot證明函數(shù)極限問題。

（這更新頻率確實o(￣▽￣)ｄ）

據(jù)陶哲軒介紹，他此前主要將GitHub Copilot用于一些“花里胡哨”的代碼補(bǔ)全，但實際情況是，如果想讓它來證明數(shù)學(xué)定理，往往需要人類的“正確指揮”。

因此，這一次的教學(xué)核心奔著一個目標(biāo)：

讓大家學(xué)會如何正確引導(dǎo)GitHub Copilot。

他從定義函數(shù)極限問題出發(fā)，依次演示了求和、求差和求積定理的證明過程，以及他在過程中遇到的問題和解決方法，全程主打一個細(xì)致。

下面具體來看。

一招鮮：Copilot代碼補(bǔ)全+人工手動調(diào)整

先說結(jié)論，和陶哲軒一直以來的觀念一致，GitHub Copilot等AI目前在數(shù)學(xué)定理證明中仍主要用于“打輔”。

Copilot能快速生成代碼框架和常見模式，對初學(xué)者尤其有用，還能提示使用已有庫函數(shù)。

但面對復(fù)雜的數(shù)學(xué)細(xì)節(jié)、特殊情況和需要創(chuàng)造性解決方案的問題時，Copilot的可靠性下降，需要大量人工干預(yù)和調(diào)整。

在他看來，復(fù)雜問題可能需要結(jié)合紙筆推導(dǎo)，確保思路正確后再進(jìn)行形式化驗證。

以下為得出結(jié)論的詳細(xì)過程。

首先，他定義了函數(shù)極限問題，即“設(shè)f是從實數(shù)到實數(shù)的函數(shù)，當(dāng)x趨近于x_??時f(x)收斂于L”。

Copilot幫忙自動補(bǔ)全了這個極限的ε-δ定義，不過由于他更喜歡用絕對值符號來表達(dá)極限的定義，所以自己又稍微修改了一下。

求和定理證明

然后他提出了第一個想要證明的問題——函數(shù)極限的求和定理證明。

如果函數(shù)f在x_??處收斂于L，函數(shù)g在x_??處收斂于M，那么f+g在x_??處收斂于L+M。

Copilot給出了正確的命題表述。

隨后在證明過程中，陶哲軒用到了大量“Copilot代碼補(bǔ)全+人工手動調(diào)整”這一模式。

比如證明的起始步驟是提取f和g收斂的ε-δ條件。這里需要特別注意δ的選取，即取δ?和δ?的最小值，以保證兩個函數(shù)的收斂性同時成立。

但Copilot最初給出的證明方式有些問題，特別是在處理δ的正性驗證（某個數(shù)學(xué)命題或結(jié)論是否為正)時不夠嚴(yán)謹(jǐn)。

同時在證明不等式部分，陶使用了計算塊（calc block）來構(gòu)建不等式鏈。雖然Copilot自動生成了基本結(jié)構(gòu)，但在絕對值符號處理和最終步驟上出現(xiàn)了偏差。

這里需要手動修正幾個關(guān)鍵點：

• 移除了多余的絕對值符號
• 修正了三角不等式的應(yīng)用
• 調(diào)整了最終表達(dá)式

另外，為了應(yīng)對數(shù)學(xué)分析中合并估計值時常遇到的ε損失問題，陶也嘗試讓Copilot采用標(biāo)準(zhǔn)解決方法（從一開始就使用ε/2來進(jìn)行論證），結(jié)果發(fā)現(xiàn)其生成的代碼中ε仍然是原來的兩倍，因此需要手動調(diào)整參數(shù)。

整體而言，他不斷在Copilot的自動補(bǔ)全和手動調(diào)整之間切換。這說明Copilot雖然能快速生成代碼框架，但關(guān)鍵的數(shù)學(xué)細(xì)節(jié)和嚴(yán)謹(jǐn)性仍需要人工把控。

不過值得一提的是，Copilot在后期提示可以使用Lean內(nèi)置的add_sub_add_comm引理，以簡化重組步驟。

這意味著，Copilot不僅能補(bǔ)全代碼，還能提醒開發(fā)者利用現(xiàn)有的庫函數(shù)。

求差定理證明

在證明了和的極限后，陶嘗試用類似方法證明差的極限。

和前面一樣，Copilot能夠生成基本正確的命題表述，并自動沿用了之前的證明框架。

不過在關(guān)鍵的一行還是出現(xiàn)了問題：它錯誤地使用了一個不存在的sub_sub_anc方法。

雖然陶嘗試通過提示讓它修正，但Copilot似乎無法記住上下文，給出的解決方案也不理想。

同時在處理代數(shù)表達(dá)式時，陶原本希望使用congruence策略來匹配等式兩邊，但這個策略過于激進(jìn)，把問題過于簡化了。

Copilot在這個環(huán)節(jié)表現(xiàn)得不太穩(wěn)定，有時會虛構(gòu)不存在的方法。

最后陶不得不手動完成這個代數(shù)恒等式的證明，因為雖然這個恒等式在所有交換群中都成立，但Lean的數(shù)學(xué)庫中并沒有現(xiàn)成的直接解決方案。

求積定理證明

最后，對于函數(shù)乘積極限定理證明，陶給Copilot的打分為B+。

總體而言，它完成了大部分工作，但在處理ε的分配和絕對值不等式時出現(xiàn)了混亂。

首先，對于乘積極限的證明，Copilot提出的策略是：

• 將f的近似誤差設(shè)為ε/(2|M|+1)
• 將g的近似誤差設(shè)為ε/(2|L|+1)

陶哲軒表示，這個思路基本正確，但在具體實現(xiàn)時出現(xiàn)了幾個問題：

其一，在驗證正性條件時，Copilot試圖使用多個特定引理，但實際上可以使用更通用的正性驗證方法。（陶手動調(diào)整了這個部分）

其二，在處理絕對值不等式時，Copilot錯誤地使用了add_lt_add方法，這個方法要求兩邊都是嚴(yán)格不等式，但實際情況中有一個等式。陶嘗試讓Copilot修正這個問題，但它給出的解決方案并不理想。

與此同時，在最終證明的以下幾個關(guān)鍵步驟中，雖然Copilot在整體框架上提供了很大幫助，但在處理這些精細(xì)的數(shù)學(xué)細(xì)節(jié)時，還是需要人工干預(yù)來確保準(zhǔn)確性。

• 使用三角不等式分解表達(dá)式
• 分別控制f(x)-L和g(x)-M的項
• 處理交叉項L(g(x)-M)和M(f(x)-L)

陶哲軒強(qiáng)調(diào)，尤其在處理不等式和絕對值運(yùn)算時，需要特別注意每個步驟的適用條件。

比如在最后階段遇到的一個bug：Copilot生成的代碼假設(shè)M是正數(shù)，而實際上并沒有這個前提條件。

對于這個問題，陶最后也花了一番功夫手動調(diào)整。并且他意識到，當(dāng)問題復(fù)雜度達(dá)到一定程度時，Copilot確實會變得不太可靠。

最后他得出結(jié)論，面臨上述情況，切換到更傳統(tǒng)的人工證明方法可能更有效。

如果我能先用紙筆寫下完整的證明思路，確保所有ε參數(shù)都正確設(shè)置，然后再進(jìn)行形式化驗證，效率會更高。

小結(jié)一下，Copilot這類工具在起步階段確實很有幫助，但關(guān)鍵在于要懂得何時使用它，何時需要切換回傳統(tǒng)方法。

One More Thing

以上教學(xué)收獲一片好評的同時，網(wǎng)友的關(guān)注點也開始逐漸跑偏——

眾人在線求更換錄音設(shè)備。

看來油管新人博主的業(yè)務(wù)還需要精進(jìn)（doge）。