[其他] 陶哲軒等式理論計畫57天完成2200萬證明

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