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操作”的表示式如下：
a∗b（一次操作）(∗)∗(a∗b)∗c（兩次操作）∗(∗(∗))a∗(b∗(c∗d))（三次操作）((∗)∗)∗(∗)((a∗b)∗c)∗(d∗e)（四次操作）
其中,,,,都是集合M中的元素，每次∗的使用都算作一次magma操作。
這樣的等式定律有4694個，由於每個定律都可能蘊含其他4693個定律（一個定律不能蘊含自身），因此總共有4694*(4694-1) = 22,028,942個可能的蘊含關係需要被證明或反駁。
這裡的蘊含關係包括“蘊含”和“反蘊含”，其中“蘊含”關係又涉及到兩種型別：
已證明的蘊含：在Lean中已經過驗證推測的蘊含：尚未在Lean中驗證，可能由人或計算機生成
更多專案細節，陶哲軒在專案日誌中，留下了非常詳細的記錄——
9天進度99.866%，大模型有用但“表現低於預期”
簡單總結“等式理論計劃”的進度，就是一個字：快。
陶哲軒本人都說：
這個專案的進度遠超我的預期。
有多快？
僅僅48小時，很大一部分蘊含關係就已“解決在望”。
專案啟動第5天，專案參與者們已經從最初的約2200萬條蘊含關係中解決了大量簡單蘊含，只剩下約300萬的數量尚待解決。
專案啟動第9天，隨著首次重大重構的完成——合作者們改進了magma的運算子號，以使Lean程式碼的編譯速度顯著加快，以及一些研究問題的推進，專案完成度一舉從87%躍升到了99.866%。
第19天，專案進度來到99.9963%。陶哲軒在他的部落格文章中提及，寫論文的事已經提上日程，並且可能包含數十名作者。
GitHub顯示該專案有45位貢獻者：
到了11月21日，也就是專案第57天，隨著主專案最後一個未解決的蘊含關係被搞定（待驗證），“等式理論計劃”目標已宣告達成。
論文可以正式開寫了。
陶哲軒透露，論文的框架早已擬好，但後續還需要大量工作來對其進行更新，並轉換為可以提交的形式。
日誌中也詳細談到了大模型工具發揮的作用。
在第一天，陶哲軒就對GitHub Copilot大加讚賞：
GitHub Copilot在處理日常任務時非常有用，比如輸入需要證明的新Lean定理，或者更新藍圖來整合最新的PR結果。
他具體舉了個例子：要將Lean轉換為LaTeX，把Lean程式碼貼上為註釋，開始敲LaTeX，GitHub Copilot就會自動補全剩下的內容。
不過，陶哲軒也坦率表示，大模型們在專案中的表現“低於預期”，更多的時候，數學家們用到的還是“經典AI”，比如自動定理證明器Vampire等。
他還提到：
專案的參與者非常多元化，包括處在職業生涯各個階段的數學家和計算機科學家，學生和業餘愛好者。Lean在整合人類和機器生成的貢獻方面表現出色。機器生成的部分在數量上是貢獻的最主要來源，不過，許多自動生成的結果最初是人類在特殊情況下得出的，之後被進一步推廣和形式化。
具體到專案中，GitHub Copilot的主要作用還是加快程式碼的編寫，而Claude則被用來幫忙建立視覺化工具，比如這個“等式瀏覽器”：
ChatGPT則更多扮演激發數學家們靈感的小助手角色。
對陶哲軒來說，ChatGPT能幫他快速掌握通用代數的一些細節。
而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta這幾位專案參與者，還透過跟ChatGPT的討論，證明1659這個等式可能具有非平凡的合流性。
主專案里程碑達成，不過“等式理論計劃”的其他衍生專案仍在進行中，比如研究在有限原群限制下的類似蘊含圖、對蘊含圖進行資料分析等等。
陶哲軒也再次強調了這一專案和AI的聯絡：
希望專案中的蘊含關係能夠作為未來AI數學工具的基準測試。
除了陶哲軒之外，專案的主要維護人還有義大利數學家Pietro Monticone和Shreyas Srinivas。
兩位都是Lean重度愛好者。
△Shreyas Srinivas主頁
Pietro Monticone還和他特倫託大學的同事們一起搞過指數3的費馬大定理的Lean版證明。
