陶哲軒宣佈“等式理論計劃”成功，57天完成2200萬+數學關係證明

57天，人類和AI合作搞定了4694個等式之間22028942個蘊含關係！

大神陶哲軒激動宣佈：等式理論計劃，成功。

“等式理論計劃”，由陶哲軒本人在2024年9月25日發起，目的是探索按蘊含關係排序的原羣（magma）等式理論空間。

特別的是，在這個項目裡，陶哲軒不僅集合了人類數學家的力量，還把AI工具納入了合作者的範圍，包括ChatGPT、Claude和GitHub Copilot。

項目發起當日就正式啓動，僅僅9天，項目進度就達到了99.866%。

而現在，在2200萬+個需要證明的蘊含關係中，8178279個已被證實，13855193個已被證僞，僅有162個還懸而未決。

按陶哲軒的說法，就是離“宣佈完全成功”基本只是“時間問題”：

什麼是“等式理論計劃”

還是先來扒一扒陶哲軒這回究竟是整了個什麼樣的活兒。

簡單說，“等式理論計劃”是指：

採用”數學家+AI（包括自動定理證明系統和大模型）+證明輔助語言Lean”這樣的協作方式，構建一個展示4694個magma等式（最多四次使用magma操作）之間所有蘊含關係的 “蘊含圖”。

首先，這個計劃的最初靈感源於陶哲軒本人對“去中心化”研究方式的暢想。

傳統上，大部分數學研究項目都由少數專業數學家（通常1~5名）進行，每個人都對自己的部分更專業，且彼此可以相互驗證。

不過也是因爲存在驗證環節，組織更大規模的數學項目（尤其是需要涉及公衆貢獻），一直具有挑戰性。

而現在，通過AI工具以及Lean這樣的證明輔助語言，數學項目的大規模協作變得可能。

打前陣的就有開源社區尋找梅森素數的成功嘗試，在這個代號GIMPS的志願項目中，任何擁有強大PC或GPU的人都可以加入尋找梅森素數。

雖然證明助手這樣的AI工具在這個項目裡用得還不多，但表達的精神是類似的。

因此，在開展等式理論計劃之前，陶哲軒就打算搞一個實驗：

在一個數學項目中，聚齊專業/業餘數學家、AI工具、證明輔助語言Lean等，一同幹大事！

受去年MathOverflow上一個等式問題的啓發，這一次，陶哲軒將目光瞄準了代數領域中的magma。

當時的問題是醬嬸兒的：

拋開具體問題不談，這裡主要想說明magma涉及等式之間的關係。

簡單來說，magma是一個代數結構，它由一個集合和一個在該集合上定義的二元運算組成，但不要求滿足任何額外的代數性質，如結合律、交換律等。

我們常見的有關magma的等式包括：

而等式理論計劃，就是要找出magma中不同等式之間的等價、推出和非推出關係。

就拿上面這11個等式來看，最終的關係圖be like：

可以看出，常量公理等式（1）蘊含了其他所有等式，即如果1成立，那麼其他等式也自動成立；而反身公理等式（11）由於最寬鬆（x=x），幾乎所有的magma都滿足這個公理。

回到計劃本身，陶哲軒等人在初始階段集中研究了那些只包含一個方程的magma定律，這些方程最多包含四個magma操作（即二元運算）。

舉個例子，如果我們有一個magma（M，∗），其中M是元素的集合，∗是定義在M上的二元運算。

則一個“最多四次使用magma操作”的表達式如下：

其中,,,,都是集合M中的元素，每次∗的使用都算作一次magma操作。

這樣的等式定律有4694個，由於每個定律都可能蘊含其他4693個定律（一個定律不能蘊含自身），因此總共有4694*(4694-1) = 22,028,942個可能的蘊含關係需要被證明或反駁。

這裡的蘊含關係包括“蘊含”和“反蘊含”，其中“蘊含”關係又涉及到兩種類型：

更多項目細節，陶哲軒在項目日誌中，留下了非常詳細的記錄——

9天進度99.866%，大模型有用但“表現低於預期”

簡單總結“等式理論計劃”的進度，就是一個字：快。

陶哲軒本人都說：

有多快？

僅僅48小時，很大一部分蘊含關係就已“解決在望”。

項目啓動第5天，項目參與者們已經從最初的約2200萬條蘊含關係中解決了大量簡單蘊含，只剩下約300萬的數量尚待解決。

項目啓動第9天，隨着首次重大重構的完成——合作者們改進了magma的運算符號，以使Lean代碼的編譯速度顯著加快，以及一些研究問題的推進，項目完成度一舉從87%躍升到了99.866%。

第19天，項目進度來到99.9963%。陶哲軒在他的博客文章中提及，寫論文的事已經提上日程，並且可能包含數十名作者。

GitHub顯示該項目有45位貢獻者：

到了11月21日，也就是項目第57天，隨着主項目最後一個未解決的蘊含關係被搞定（待驗證），“等式理論計劃”目標已宣告達成。

論文可以正式開寫了。

陶哲軒透露，論文的框架早已擬好，但後續還需要大量工作來對其進行更新，並轉換爲可以提交的形式。

日誌中也詳細談到了大模型工具發揮的作用。

在第一天，陶哲軒就對GitHub Copilot大加讚賞：

他具體舉了個例子：要將Lean轉換爲LaTeX，把Lean代碼粘貼爲註釋，開始敲LaTeX，GitHub Copilot就會自動補全剩下的內容。

不過，陶哲軒也坦率表示，大模型們在項目中的表現“低於預期”，更多的時候，數學家們用到的還是“經典AI”，比如自動定理證明器Vampire等。

他還提到：

具體到項目中，GitHub Copilot的主要作用還是加快代碼的編寫，而Claude則被用來幫忙創建可視化工具，比如這個“等式瀏覽器”：

ChatGPT則更多扮演激發數學家們靈感的小助手角色。

對陶哲軒來說，ChatGPT能幫他快速掌握通用代數的一些細節。

而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta這幾位項目參與者，還通過跟ChatGPT的討論，證明1659這個等式可能具有非平凡的合流性。

主項目里程碑達成，不過“等式理論計劃”的其他衍生項目仍在進行中，比如研究在有限原羣限制下的類似蘊含圖、對蘊含圖進行數據分析等等。

陶哲軒也再次強調了這一項目和AI的聯繫：

除了陶哲軒之外，項目的主要維護人還有意大利數學家Pietro Monticone和Shreyas Srinivas。

兩位都是Lean重度愛好者。

△Shreyas Srinivas主頁

Pietro Monticone還和他特倫託大學的同事們一起搞過指數3的費馬大定理的Lean版證明。