機器之心報道
編輯: 蛋醬、小舟
嘗鮮 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