這個五一假期，世界頂級數學家是如何度過的？

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

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

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

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

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

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

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

現在，這個心愿實現了。

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

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

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

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

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

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

與此同時，陶哲軒還放出了與 ChatGPT 的對話過程，不難發現，對話過程還是蠻長的。

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

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

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

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

ChatGPT 也給出了回答：

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

「如何在與當前 python 文件相同的目錄下導入 python 文件？」

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

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

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

陶哲軒還建議大家如果想要開發這類軟件，最好是數學家與專業程序員以協作的方式進行，這樣才能優勢互補。

「這當然是一個極其不優雅的證明，但優雅并非重點，重點在于它是自動化的。」

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