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
參考鏈接：
[ 1 ] https://mathstodon.xyz/@tao/113522452070896956
[ 2 ] https://teorth.github.io/equational_theories/
[ 3 ] https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/
