陶哲軒宣布“等式理論計劃”成功，人類AI協作，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操作”的表達式如下：
- 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版證明。
GitHub：https://github.com/teorth/equational_theories
