這個(gè)五一假期，世界頂級數(shù)學(xué)家是如何度過的？

菲爾茲獎得主陶哲軒，似乎是忙著發(fā)布自己的開源項(xiàng)目：「我在大模型的協(xié)助下編寫了一個(gè)概念驗(yàn)證軟件工具，用于驗(yàn)證涉及任意正參數(shù)的給定估計(jì)是否成立（在常數(shù)因子范圍內(nèi)）。」

項(xiàng)目地址：https://github.com/teorth/estimates

在這個(gè)項(xiàng)目中，陶哲軒開發(fā)了一個(gè)用于自動（或半自動）證明分析中估計(jì)值的框架。估計(jì)值是 X?Y（在漸近記法中表示 X=O (Y)）或 X?Y（在漸近符號中表示 X=o (Y)）形式的不等式。

為什么要做這樣一個(gè)工具？這就要從近期陶哲軒和 Bjoern Bringmann（陶哲軒曾經(jīng)的博士生，現(xiàn)為普林斯頓大學(xué)助理教授）的討論說起。

對于代數(shù)、微積分和數(shù)值分析等領(lǐng)域的許多數(shù)學(xué)任務(wù)來說，符號數(shù)學(xué)軟件包已經(jīng)非?！赴l(fā)達(dá)」了。但目前還沒有類似的復(fù)雜工具來驗(yàn)證漸近估計(jì) —— 在損失不變的情況下，對于任意大的參數(shù)都應(yīng)該成立的不等式。尤其重要的是函數(shù)估計(jì)，其中參數(shù)涉及一個(gè)未知函數(shù)或序列（存在于某個(gè)合適的函數(shù)空間，如一個(gè)空間）。

陶哲軒將二人的討論結(jié)果寫成了一篇博客，重點(diǎn)討論了更簡單的漸近估計(jì)情況，即涉及有限數(shù)量的正實(shí)數(shù)，并使用加、乘、除、指數(shù)、最小值和最大值（但不包括減法）等算術(shù)運(yùn)算進(jìn)行組合。

「我過去曾希望能有一個(gè)工具能夠自動判斷此類估計(jì)是否成立（如果成立，則提供證明；如果不成立，則提供漸近反例）?！?/span>

現(xiàn)在，這個(gè)心愿實(shí)現(xiàn)了。

我們都知道，陶哲軒非常愛好使用大模型來輔助解決數(shù)學(xué)問題。過去的大多數(shù)情況是完成比較簡單的編碼任務(wù)，例如計(jì)算然后繪制一些稍微復(fù)雜的數(shù)學(xué)函數(shù)，或者對某些數(shù)據(jù)集進(jìn)行一些基本的數(shù)據(jù)分析。

這次，他決定給自己一個(gè)更具挑戰(zhàn)性的任務(wù)：編寫一個(gè)可以處理上述形式不等式的驗(yàn)證器。

舉個(gè)例子，一個(gè)典型的不等式可能是弱算術(shù)平均 - 幾何平均不等式。

其中 abc 是任意正實(shí)數(shù)，這里的表示我們愿意在估計(jì)中丟失一個(gè)未指定的（乘性）常數(shù)。

原則上，這類形式的簡單不等式可以通過強(qiáng)力的案例拆分自動解決。單個(gè)這類的不等式都不太難手工求解，但有些應(yīng)用需要檢驗(yàn)大量這樣的不等式，或者將其拆分成大量案例。這項(xiàng)任務(wù)似乎非常適合自動化，尤其是在現(xiàn)代技術(shù)的幫助下。

陶哲軒這次用到的 AI 工具仍然是 ChatGPT。經(jīng)過大約四個(gè)小時(shí)的編程，在大模型的頻繁協(xié)助下，他順利做出了一個(gè)概念驗(yàn)證工具。

與此同時(shí)，陶哲軒還放出了與 ChatGPT 的對話過程，不難發(fā)現(xiàn)，對話過程還是蠻長的。

鏈接：https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8

一開始，陶哲軒就對 ChatGPT 提出了自己的需求：「我想編寫一些 Python 類來操作符號表達(dá)式。并且希望有一個(gè)表示變量的類，比如 x、y、z…… 你能幫我編寫一些具有這種功能的基礎(chǔ)類來入門嗎？」

ChatGPT 思考了 6 秒鐘就給出了答案。

這一步完成之后，下一輪對話開始，陶哲軒接著追問「我看到你用 add 實(shí)現(xiàn)了 + 操作，真棒。那么，實(shí)現(xiàn) * 和 / 的對應(yīng)方法是什么呢？」

ChatGPT 也給出了回答：

在整個(gè)過程中，陶哲軒不斷詢問，ChatGPT 也做到了有問必答，不管是簡單的問題，還是復(fù)雜的問題，ChatGPT 都給解決了：

「如何在與當(dāng)前 python 文件相同的目錄下導(dǎo)入 python 文件？」

最終，在 ChatGPT 的大力協(xié)助下，陶哲軒完成了這個(gè)概念驗(yàn)證軟件工具。

其實(shí)，在眾多知名數(shù)學(xué)家中，陶哲軒是較早接受并發(fā)現(xiàn) ChatGPT 這類 AI 大模型數(shù)學(xué)價(jià)值的一個(gè)。他曾預(yù)測「如果使用得當(dāng)，到 2026 年，AI 將成為數(shù)學(xué)研究和許多其他領(lǐng)域值得信賴的合著者。」

陶哲軒不止一次借助大模型進(jìn)行研究，他曾在 GPT-4 的幫助下成功解決了一個(gè)數(shù)學(xué)證明題（GPT4 提出了 8 種方法，其中 1 種成功解決了問題），還在 AI 的幫助下發(fā)現(xiàn)了自己論文中的一處隱藏 bug。

陶哲軒還建議大家如果想要開發(fā)這類軟件，最好是數(shù)學(xué)家與專業(yè)程序員以協(xié)作的方式進(jìn)行，這樣才能優(yōu)勢互補(bǔ)。

「這當(dāng)然是一個(gè)極其不優(yōu)雅的證明，但優(yōu)雅并非重點(diǎn)，重點(diǎn)在于它是自動化的?！?/span>

回顧整個(gè)過程，我們可以從陶哲軒的經(jīng)歷中得到一些啟發(fā)，對大模型的開發(fā)使用，或許只是冰山一角，更多的功能等著大家去解鎖。