今年6月，陶哲軒曾在博客中預言，2026年，AI將與搜索和符號數(shù)學工具相結合，成為數(shù)學研究中值得信賴的合著者。

這個預言，如今已經(jīng)愈發(fā)成真。

就在6月底，加州理工、英偉達、MIT等機構的學者，曾構建了一個基于開源LLM的定理證明器。

最近，陶哲軒又發(fā)現(xiàn)，在使用Lean進行自然數(shù)游戲研究時，GPT-4竟然也起到一些作用。

在AI的輔助下，他得到了關于有限多個實變量不等式理論的成果，論文很快就會發(fā)在arXiv上。

圖片

如何用GPT-4研究自然數(shù)游戲

什么是自然數(shù)游戲？

圖片

這個游戲，神奇地展示了歸納的力量。

如圖所示，我們從藍色節(jié)點上輸入，而灰色節(jié)點上方的所有結點都完成時，灰色節(jié)點將變?yōu)樗{色。

在這個過程中，我們當然可以隨時嘗試任何級別的節(jié)點，但如果它是灰色的，我們可能就沒有足夠的知識來完成這個節(jié)點。

引理：對于所有自然數(shù)x、y和z都有xy+z=xy+z。證明開始！

在自然數(shù)游戲中，我們就會在定理證明器Lean中，得到自己的一個自然數(shù)版本——mynat。這個自然數(shù)滿足了數(shù)學歸納定理，以及其他原理（比如皮亞諾公理）。

圖片

不過，問題在于，目前還沒有人證明這些關于自然數(shù)的定理，比如，你可以定義加法，但還沒有人證明x + y = y + x。

皮亞諾公理

而自然數(shù)游戲，就需要你解決游戲中的關卡，用Lean定理證明器來證明數(shù)學定理。

我們證明了n+0=n，這個證明被稱為add_zero。但并不能證明zero_add，0+n=n。這兩個定理不是一樣嗎？并非如此！事實上x + y = y + x，這是加法世界的BOSS級難題。

陶哲軒是出于怎樣的機緣巧合，開始玩自然數(shù)游戲的呢？

原來，他是在IPAM機器輔助證明研討會上看到過幾次Lean的演示，并且被建議玩一玩自然數(shù)游戲，來熟悉Lean中用于證明定理的基本語法和策略。

讓陶哲軒感到驚喜的是，這個游戲越玩越熟悉，因為它證明的結果和自己寫的本科實分教材前幾章的結果分成相似。

圖片

比如，從皮亞諾公理建立基本的算術事實，例如乘法的交換性和結合性。

另外，自然數(shù)游戲還讓他想起了自己編碼的邏輯游戲。

才玩了三個小時，陶哲軒就已經(jīng)到達了「高級乘法」世界。他表示，在以后的空閑時間里他會繼續(xù)玩這個游戲。

圖片

高級乘法世界：證明兩個非零自然數(shù)的乘積為非零：a≠0 → b≠0 → a*b≠0

當然，GPT-4也知道Lean，它可以提供一些有用的回答。

不過，因為自然數(shù)游戲中可用的工具集很有限，所以GPT-4對于這個游戲沒有直接的幫助，因為它提出的解決方案中涉及的方法，通常還沒有被納入游戲中。

不過，當他開始使用Lean的時候，GPT-4就變得非常有幫助了。

圖片

隨著關卡變得越來越難，GPT的作用開始逐漸顯現(xiàn)出來。

在Z顯而易見是X和Y的結果的情況下，如果向GPT提問——

如果我已經(jīng)知道X和Y，該如何證明Z呢？

這個過程就解決了各種微妙的語法問題，否則這些問題會十分令人沮喪。

圖片

而且，陶哲軒發(fā)現(xiàn)，自然數(shù)游戲中包含的Lean庫，似乎比文件中宣稱的要多得多。

GitHub Copilot，讓我不安

總之，AI工具輔助研究數(shù)學的奇跡，一次次讓陶哲軒稱贊不已，甚至發(fā)展到了讓他「不安」。

前不久陶哲軒發(fā)現(xiàn)，GitHub Copilot已經(jīng)能夠預測到自己文章中數(shù)學論證的步驟了。

圖片

在10月初，陶哲軒表示，Github Copilot的能力驚艷到他了。

而且他強調(diào)，并不是它的編碼能力，而是它編碼之外的補充其他內(nèi)容的能力，經(jīng)常能讓他喜出望外。

最近，他又稱贊到——

我發(fā)現(xiàn)Github Copilot在我最近撰寫博客文章的過程中出奇地有幫助。它能夠正確預測該帖子中數(shù)學論證的幾個步驟；在下面給出的示例中，我將積分分成三部分，并描述了如何估計第一部分，然后copilot正確地說明了如何估計其余兩部分。

陶哲軒給出的例證

只要簡單說明一下如何對第一部分進行估計，剩下的工作GitHub Copilot就能完成了，這也太驚艷了！

對此，陶哲軒的評價是：「Copilot的性能給我留下了深刻的印象（并且讓我有點不安）」。

他補充說「雖然其中的許多建議并不那么合適，我估計Copilot可能建議了十幾句話，最終以某種形式出現(xiàn)在我的博客文章中。」

而他說的博客文章就是這篇關于「非負量的和或積分的上界」。

圖片

博文地址：https://terrytao.wordpress.com/2023/09/30/bounding-sums-or-integrals-of-non-negative-quantities/

估計某個量的大小，是數(shù)分、概率論、組合學等領域中的常見問題，如估計函數(shù)、序列、結合等的和或積分。

因此陶哲軒這篇估計非負量的和或積分上界，探討的正是數(shù)學領域的重要問題。

圖片

陶哲軒在博客中總結了3種估算大量非負量和以及積分的方法，如算術平均值-幾何平均值不等式、Holder不等式、Markov不等式等。

圖片

其中的內(nèi)容和代碼沒有關系，但是Github Copilot依然給出了讓陶哲軒都感到驚嘆的內(nèi)容建議。

圖片

能讓陶哲軒都感到有點不安的Github Copilot，源于Github和OpenAI的合作。

它主要功能是利用生成式AI的能力為程序提供編碼的建議，自動補充等編碼功能。而之所以它有如此強大的功能，和背后微軟，OpenAI的大量投入是分不開的。

最近外媒報道，微軟提供的Github Copilot每月10刀的訂閱服務，在算力成本上，每個用戶要讓微軟虧損20美元/月。

圖片

文章地址：https://www.wsj.com/tech/ai/ais-costly-buildup-could-make-early-products-a-hard-sell-bdd29b9f?mod=followamazon

這些服務成本如此高昂的原因之一，是使用了最強大的AI模型，與普通的軟件或云服務相比，這些模型需要更多的電力，并對處理器的運行造成更大的壓力。

文章中甚至將現(xiàn)在的AI工具的能力和成本做了一個讓人繃不住的比喻：

「用AI去做文章總結就像開著蘭博基尼去送披薩一樣」。

足見現(xiàn)在科技巨頭們，為了讓用戶充分享受AI帶來的便利，真的是下了血本！

所以讓陶哲軒驚嘆的Github Copilot能在編碼之外還有如此強大的能力，也似乎不那么奇怪了。

AI如何輔助數(shù)學研究

顯然，現(xiàn)在所有人都已經(jīng)意識到：AI具有巨大潛力，它可以通過指導猜想生成、協(xié)助形式化數(shù)學等方式為數(shù)學發(fā)展做出貢獻。

在9月26日舉行的一場關于使用AI輔助數(shù)學推理的網(wǎng)絡研討會上，眾數(shù)學大咖云集，一起討論了人工智能技術如何用于推進數(shù)學科學，跨學科合作如何開辟新的機會。

陶哲軒也參與了會議，并結合自己與AI合作的經(jīng)歷談了自己的觀點。

圖片

大會對于AI輔助數(shù)學研究，AI專家和數(shù)學家協(xié)作配合的新機會和新挑戰(zhàn)，都展開了充分地討論，可謂是干貨滿滿：

嘗試應用機器學習方法來輔助或完成形式數(shù)學論證，現(xiàn)在已經(jīng)是人工智能應用的一個獨特領域

AI在輔助數(shù)學研究中的獨特之處在于，數(shù)學具有一種自我驗證的方法，可以用來檢查AI產(chǎn)生的結果，而其他AI任務通常需要人類參與來評估反饋的質(zhì)量。

數(shù)學表達本身具有一種內(nèi)在的準確性，因此機器學習在數(shù)學領域能夠在數(shù)據(jù)相對稀缺的情況下有效地推進工作，這使得AI在數(shù)學領域具備明顯的優(yōu)勢。

在研討會上，多位數(shù)學領域?qū)＜疫M行了知識分享和交流。

圖片

在使用機器學習協(xié)助數(shù)學發(fā)現(xiàn)方面,會議中數(shù)學家Heather提到了具體的幾個例子:

圖片

(1) DeepMind和數(shù)學家合作，利用機器學習從大量數(shù)據(jù)中尋找模式，形成了關于模形的新猜想。

(2) Sutherland等數(shù)學家也使用機器學習在模形式的工作中找到了新公式。

(3) Adam Wagner使用機器學習來尋找圖論問題的反例。

(4) Javier Pena利用機器學習找到偏微分方程近似的數(shù)值解,以方便后續(xù)的嚴格數(shù)值方法的推進。

在使用AI輔助證明方面,會議提到形式化證明可以將一個大證明分解成小塊,不同人可以負責不同部分。

圖片

這可能會開啟新的科研協(xié)作模式——計算機可以自動化證明中的某些步驟，已經(jīng)有許多前沿的數(shù)學領域使用了這種模式。

這種形式化證明的過程有利于數(shù)學家以新方式與AI進行創(chuàng)造性的互動。

這也體現(xiàn)了AI協(xié)助數(shù)學發(fā)現(xiàn)和傳統(tǒng)數(shù)學研究的不同：既有大公司提供計算資源的大規(guī)模合作，也有小規(guī)模的個人之間的合作探索。

學界需要對這些不同的合作模式保持開放。

圖片

會議中，還有多位學者討論了AI在數(shù)學翻譯中的應用

數(shù)學翻譯是指將一個數(shù)學問題從一個領域翻譯到另一個領域的等價表達,這是數(shù)學家解決問題的基本工具之一。

數(shù)學家以一個圖論問題為例。圖論問題可以翻譯成代數(shù)問題，兩者邏輯上是等價的，但表達上的術語和形式明顯不同。

AI轉換工具可以將一個看似毫無頭緒的問題，轉化成一個可以用已有技術來解決的問題。

還有學者進一步指出，證明思路到形式證明的轉換，以及形式證明到實際算法的轉換，也是一種翻譯過程。

鑒于AI在不同語言之間的翻譯上取得了巨大進展，未來可以研究如何應用機器學習來實現(xiàn)數(shù)學領域內(nèi)的翻譯。

例如將不完整的證明草圖自動翻譯成可證明的形式表達。這是當前一個非常有前景的研究方向。

會議中多位數(shù)學家也強調(diào)了。由于數(shù)學翻譯能顯著拓展問題解決的視角，應用機器學習來實現(xiàn)數(shù)學翻譯將可能大大推進數(shù)學研究。

圖片

AI專家和數(shù)學家進行跨界合作，需要面對的差異和挑戰(zhàn)

AI界和數(shù)學界，存在著諸多差異。

比如，機器學習研究者習慣處理大規(guī)模數(shù)據(jù)集，而數(shù)學家習慣于處理相對較少的數(shù)據(jù)。機器學習研究者注重在一類任務上的平均表現(xiàn)，而數(shù)學家則更關注單個案例的解釋。

另外，兩者的出版文化不同，機器學習界會公開發(fā)表絕大部分研究內(nèi)容，數(shù)學界則不然。機器學習界普遍第一作者為主要貢獻者，數(shù)學界作者順序就比較隨機。

大規(guī)模合作項目的學術貢獻認定上，二者也存在差異。形式化研究使得每個參與者只負責一小塊，如何評價貢獻是一個新問題。

還有一個差異，是資源獲取方式。

機器學習需要大數(shù)據(jù)集和計算資源，數(shù)學家對這方面的需求就相對較少。如何使各界研究者公平獲取資源也會是一個問題。開源文化不同。機器學習界更看重開源共享,而數(shù)學界不一定。如何處理二者關系需要考量。

由于這是一個全新的交叉領域,雙方在一些根本理念和工作方式上存在差異，需要在合作中加以認識和調(diào)適，以實現(xiàn)更好的協(xié)同效果。

參考資料：

https://mathstodon.xyz/@tao/111206761117553482