陶哲軒「喂飯級」AI 教程來了！只用 GitHub Copilot 證明函數極限問題

一水 發自 凹非寺

量子位 | 公眾號 QbitAI

影片新人博主陶哲軒又更新了！這次是「喂飯級」AI教程——

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

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

據陶哲軒介紹，他此前主要將GitHub Copilot用於一些「花里胡哨」的代碼補全，但實際情況是，如果想讓它來證明數學定理，往往需要人類的「正確指揮」。

因此，這一次的教學核心奔著一個目標：

讓大家學會如何正確引導GitHub Copilot。

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

下面具體來看。

一招鮮：Copilot代碼補全+人工手動調整

先說結論，和陶哲軒一直以來的觀念一致，GitHub Copilot等AI目前在數學定理證明中仍主要用於「打輔」。

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

但面對複雜的數學細節、特殊情況和需要創造性解決方案的問題時，Copilot的可靠性下降，需要大量人工干預和調整。

在他看來，複雜問題可能需要結合紙筆推導，確保思路正確後再進行形式化驗證。

以下為得出結論的詳細過程。

首先，他定義了函數極限問題，即「設f是從實數到實數的函數，當x趨近於x_𝜃時f(x)收斂於L」。

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

求和定理證明

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

如果函數f在x_𝜃處收斂於L，函數g在x_𝜃處收斂於M，那麼f+g在x_𝜃處收斂於L+M。

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

隨後在證明過程中，陶哲軒用到了大量「Copilot代碼補全+人工手動調整」這一模式。

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

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

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

這裏需要手動修正幾個關鍵點：

• 移除了多餘的絕對值符號

• 修正了三角不等式的應用

• 調整了最終表達式

另外，為了應對數學分析中合併估計值時常遇到的ε損失問題，陶也嘗試讓Copilot採用標準解決方法（從一開始就使用ε/2來進行論證），結果發現其生成的代碼中ε仍然是原來的兩倍，因此需要手動調整參數。

整體而言，他不斷在Copilot的自動補全和手動調整之間切換。這說明Copilot雖然能快速生成代碼框架，但關鍵的數學細節和嚴謹性仍需要人工把控。

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

這意味著，Copilot不僅能補全代碼，還能提醒開發者利用現有的庫函數。

求差定理證明

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

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

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

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

同時在處理代數表達式時，陶原本希望使用congruence策略來匹配等式兩邊，但這個策略過於激進，把問題過於簡化了。

Copilot在這個環節表現得不太穩定，有時會虛構不存在的方法。

最後陶不得不手動完成這個代數恒等式的證明，因為雖然這個恒等式在所有交換群中都成立，但Lean的數學庫中並沒有現成的直接解決方案。

求積定理證明

最後，對於函數乘積極限定理證明，陶給Copilot的打分為B+。

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

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

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

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

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

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

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

與此同時，在最終證明的以下幾個關鍵步驟中，雖然Copilot在整體框架上提供了很大幫助，但在處理這些精細的數學細節時，還是需要人工干預來確保準確性。

• 使用三角不等式分解表達式

• 分別控制f(x)-L和g(x)-M的項

• 處理交叉項L(g(x)-M)和M(f(x)-L)

陶哲軒強調，尤其在處理不等式和絕對值運算時，需要特別注意每個步驟的適用條件。

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

對於這個問題，陶最後也花了一番功夫手動調整。並且他意識到，當問題複雜度達到一定程度時，Copilot確實會變得不太可靠。

最後他得出結論，面臨上述情況，切換到更傳統的人工證明方法可能更有效。

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

小結一下，Copilot這類工具在起步階段確實很有幫助，但關鍵在於要懂得何時使用它，何時需要切換回傳統方法。

One More Thing

以上教學收穫一片好評的同時，網民的關注點也開始逐漸跑偏——

眾人在線求更換錄音設備。

看來油管新人博主的業務還需要精進（doge）。

參考鏈接：

[1]https://www.youtube.com/watch?v=c1ixXMtmfS8

[2]https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/limits.lean