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

不禁好奇，是什么樣的數(shù)學(xué)定理呢？

根據(jù)陶哲軒的介紹，他最近在包含有限多個(gè)實(shí)變量的不等式理論中有一個(gè)完成的示例結(jié)果，并很快會發(fā)表在 arXiv 上。

因此，他最終決定開始了解 Lean4 交互式證明系統(tǒng)，使用必要的輔助 AI 工具（GPT-4）來幫助自己來使用。他希望能夠?qū)崿F(xiàn)相當(dāng)簡單的形式化。

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

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

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

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

大約 3 個(gè)小時(shí)后，陶哲軒玩到了「高級乘法」，并計(jì)劃之后在空閑時(shí)間繼續(xù)玩下去。

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

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

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

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

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

看來，要想回答這個(gè)問題，陶哲軒的大模型試驗(yàn)之旅還將繼續(xù)下去。