近幾個月來，著名數學家陶哲軒熱衷于用 ChatGPT、GPT-4 等 AI 工具輔助解決數學問題。我們也一直在持續地關注，這不今天又看到了他使用 GPT-4 來幫助自己證明數學定理。

不禁好奇，是什么樣的數學定理呢？

根據陶哲軒的介紹，他最近在包含有限多個實變量的不等式理論中有一個完成的示例結果，并很快會發表在 arXiv 上。

因此，他最終決定開始了解 Lean4 交互式證明系統，使用必要的輔助 AI 工具（GPT-4）來幫助自己來使用。他希望能夠實現相當簡單的形式化。

我們也搜到了一篇陶哲軒的關于麥克勞林（Maclaurin）型不等式的論文，不知道是不是同一篇。

論文地址：https://browse.arxiv.org/pdf/2310.05328.pdf

陶哲軒在 IPAM 機器輔助證明研討會上看過幾次 Lean 演示，在那里有人建議他玩一玩自然數游戲，以此熟悉 Lean 中用來證明定理的基本語法和策略。

他發現自己很能上手這個游戲，其中證明結果與其本科實分析書中前面的章節非常相似，比如根據皮亞諾公理建立乘法交換律和結合律等基本算數事實。此外還讓他想起了自己在《QED-an interactive textbook》中編碼過的邏輯游戲。

大約 3 個小時后，陶哲軒玩到了「高級乘法」，并計劃之后在空閑時間繼續玩下去。

自然數游戲地址：https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game

然而，考慮到自然數游戲中有限的可用工具集，陶哲軒還沒有發現 GPT-4 對解答該游戲直接有用，它給出的解答方案通常包含未納入游戲的方法。不過，他發現 GPT-4 當然對 Lean 很有幫助，他可以從中得到有關問題的有用答復。

隨著關卡越來越難，GPT-4 肯定會更有用。比如，在 Z 是 X 的明顯結果以及 Y 正在解決各種微妙語法問題（否則這些問題會非常令人沮喪）的情況下，問它「如果我知道了 X 和 Y，如何證明 Z 呢？」。陶哲軒發現，自然數游戲似乎擁有比文檔實際披露的更多的 lean 庫。

對于陶哲軒的嘗試，有網友表示很酷。Lean 非常好。有很多工作需要編寫經過驗證的證明檢查器，比如 SAT、SMT、sharp-SAT 等也使用 Lean。

還有人問陶哲軒，「如果讓你猜的話，LLM 需要多少年才能擁有超越全人類的寫證明能力呢？」

看來，要想回答這個問題，陶哲軒的大模型試驗之旅還將繼續下去。