新火種
2024-11-24 
陶哲軒宣布“等式理論計劃”成功，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大加贊賞：
他具體舉了個例子：要將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版證明。
相關推薦
- 免責聲明
- 本文所包含的觀點僅代表作者個人看法，不代表新火種的觀點。在新火種上獲取的所有信息均不應被視為投資建議。新火種對本文可能提及或鏈接的任何項目不表示認可。 交易和投資涉及高風險，讀者在采取與本文內容相關的任何行動之前，請務必進行充分的盡職調查。最終的決策應該基于您自己的獨立判斷。新火種不對因依賴本文觀點而產生的任何金錢損失負任何責任。
