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

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

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

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

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

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

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

下面具體來(lái)看。

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

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

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

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

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

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

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

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

求和定理證明

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

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

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

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

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

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

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

這里需要手動(dòng)修正幾個(gè)關(guān)鍵點(diǎn)：

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

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

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

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

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

求差定理證明

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

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

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

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

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

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

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

求積定理證明

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

One More Thing

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

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

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