嚐鮮 GPT-4 之後，陶哲軒又用上了 Github Copilot。

這一次，他的試用場景是學習 Lean 語言並利用其形式化數學定理。

對於大模型來說，形式化的定理證明也算一種挑戰。形式化證明本質上是一種計算機程序，但與 C++ 或 Python 中的傳統程序不同，證明的正確性可以用證明助手（比如 Lean 語言）來驗證。定理證明是程式碼生成的一種特殊形式，在評估上非常嚴格，沒有讓模型產生幻覺的空間。

而陶哲軒提到的定理，來自 10 月 9 日的一篇論文：

論文中的這個證明只有不到一頁，但陶哲軒的形式化證明使用了 200 行 Lean 語言。

舉例來說，在論文中，陶哲軒只是斷言對於任意 a>0 的情況，

在實數上是凸的，因為這是一個常規的微積分練習，然後調用了 Jensen 不等式，但寫出所有細節用了大約 50 行程式碼。

陶哲軒表示，Github copilot 能夠正確預測各種例行驗證的多行程式碼，並從定理的名字等線索中推斷出他想要的方向，這種能力是「不可思議」的。

Lean 的「重寫」策略是不可或缺的，它可以通過有針對性的替換來修改冗長的假設或目標，無需完整地鍵入表達式就能對其進行操作。

「在用 LaTeX 撰寫證明時，我經常粗略地模擬這種方法，將我要處理的冗長表達式從一行剪切粘貼到下一行，然後進行有針對性的編輯，但這有時會導致錯字在文件中多行傳播，因此能以自動和可驗證的方式進行重寫是件好事。」

論文中還提到一個不等式，即對於任意的 k, l, n，滿足

，則

陶哲軒表示下一個目標就是建立該不等式的簡單版本，即論文中的不等式 (1.8)：

這部分的證明主要還是利用微積分的知識，但有一個難點是需要使用漸近符號。陶哲軒表示後續的論證雖然會很耗時，但並不是特別困難。

但目前的工具仍有一些侷限性，例如，重寫涉及綁定變數（如數列中的求和變數）的表達式並不總是很容易完成。他期待著有一天，人們可以簡單地要求自然語言 LLM 進行此類轉換……

參考連結：https://mathstodon.xyz/@tao/111271244206606941