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

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

項目地址：https://github.com/teorth/estimates

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

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

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

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

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

現(xiàn)在，這個心愿實現(xiàn)了。

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

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

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

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

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

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

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

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

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

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

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

ChatGPT 也給出了回答：

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

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

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

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

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

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

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

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