★置頂zzllrr小樂公眾號（主頁右上角）數(shù)學(xué)科普不迷路！

近日，陶哲軒終于在arxiv上提交了一篇題為“等式理論項目：大規(guī)模促進協(xié)作數(shù)學(xué)研究”

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

該項目為未來更多的大規(guī)模數(shù)學(xué)家社區(qū)合作項目提供了優(yōu)秀示范。

作者：陶哲軒（博客及項目文檔、論文等）2025-12-9

譯者：zzllrr小樂（數(shù)學(xué)科普公眾號）2025-12-10

該項目（Equational Theories Project，ETP，原群等式定律項目）的核心目標是，確定 4694 條階≤4 的原群（magma，有封閉二元運算的集合）等式定律之間的全部蘊含關(guān)系（共 4694×(4694-1) = 22028942 條邊），包括一般原群和有限原群的蘊含關(guān)系，所有結(jié)果通過 Lean 形式化驗證（目前僅剩一個蘊含關(guān)系成立與否未知：有限原群情況下，定律E677是否蘊含定律E255）。

上圖可視化了 Equational Theories 項目的完整蘊含關(guān)系圖。每個像素表示兩條定律之間的關(guān)系：藍色像素表示第一個（橫坐標）蘊含第二個（縱坐標）。紅色像素表示不蘊含。亮色表示顯式證明或反例；深色表示結(jié)果是間接的。

將蘊含關(guān)系圖可視化為哈斯圖（向下邊表示子集關(guān)系，向上邊表示蘊含關(guān)系），等價類折疊為單個節(jié)點，支持搜索參數(shù)篩選圖的子集，可顯示完整蘊含關(guān)系圖（規(guī)模較大，導(dǎo)航難度高）

陶哲軒在項目日志中坦言，“我也很高興看到有非常廣泛的貢獻者，從數(shù)學(xué)或計算機科學(xué)領(lǐng)域的專業(yè)研究人員和研究生，到其他專業(yè)、擁有本科數(shù)學(xué)教育背景的人士。這是高度結(jié)構(gòu)化協(xié)作項目的主要優(yōu)勢之一——項目中存在模塊化的子任務(wù)，可以由不一定具備完整理解整個項目技能的人作有效貢獻。一方面，我們從沒有Lean專業(yè)知識的資深數(shù)學(xué)家那里獲得了重要見解；我們正在招募志愿者，將藍圖中陳述的單一定理形式化，這條定理只需要相對較窄的數(shù)學(xué)專業(yè)知識；我們也獲得了大量寶貴的技術(shù)支持，用于維護Github后端和各種用戶界面UI前端，這些前端對高級數(shù)學(xué)或Lean技術(shù)幾乎不具備經(jīng)驗。當(dāng)然，現(xiàn)在大多數(shù)貢獻遠遠超出我自己的技能能輕松完成的范圍，看到項目遠遠超出我最初的貢獻，真是令人愉快。”

關(guān)于大模型（LLM）及AI在項目中的作用，陶哲軒在其博客中也提到，現(xiàn)代AI人工智能工具在該項目中并未發(fā)揮重要作用（但該項目大部分于2024年完成，早于最新可用的先進模型）；雖然它們能解決許多問題，但“老式人工智能”（GOFAI，例如 Vampire 或 Mace9）自動化定理證明器運行成本低得多，而且已經(jīng)處理了先進 AI 工具所能處理的絕大多數(shù)問題。但他說可以想象，這些工具在未來類似項目中會扮演更突出的角色。在其論文中，陶哲軒透露該項目廣泛使用自動定理證明器完成核心目標，但現(xiàn)代大語言模型（LLM）的應(yīng)用較為有限：

• 輔助編寫圖形用戶界面代碼；

• 提供代碼自動補全（如 GitHub Copilot）

• 猜測定律的完整重寫系統(tǒng)（如 E3523 的重寫系統(tǒng)）

但在困難蘊含關(guān)系的解決上，LLM 未提供超越人類參與者的有效建議。

該項目成功的借鑒意義

借助現(xiàn)代協(xié)作平臺和證明輔助工具，可通過眾包方式對大規(guī)模數(shù)學(xué)命題空間（本項目為等式定律的蘊含關(guān)系）進行探索。盡管無單一工具或方法能覆蓋整個空間，且許多非形式化證明存在非平凡錯誤，但通過多種技術(shù)的組合、參與者的協(xié)作及 Lean 的證明驗證，可將這些部分且可能存在錯誤的貢獻整合為完整、經(jīng)過驗證的蘊含關(guān)系圖描述。

整個項目的組成部分 =在線協(xié)作研究（類似“Polymath”風(fēng)格，但這次是通過Lean Zulip進行）

+形式驗證（Lean）

+現(xiàn)代項目管理工具（Github）

+數(shù)據(jù)可視化工具（Graphviz + 自制工具）

+自動化（主要是自動化定理證明器和后臺數(shù)據(jù)管理）

+廣泛多元的參與（學(xué)術(shù)/非學(xué)術(shù)、初級/高級、數(shù)學(xué)/計算機/軟件工程等）

+社區(qū)標準（大多用 CONTRIBUTING.md 來規(guī)范）

在最終論文中，陶哲軒總結(jié)出該項目成功的關(guān)鍵因素：

• 目標明確：核心目標清晰，有明確的結(jié)束條件和量化進度指標，引導(dǎo)參與者聚焦關(guān)鍵任務(wù)

• 高度模塊化：參與者可專注于特定蘊含關(guān)系和證明技術(shù)，無需依賴其他貢獻，支持并行化和去中心化協(xié)作

• 低準入門檻：問題無需高深數(shù)學(xué)知識或形式化證明經(jīng)驗，吸引廣泛背景的參與者

• 難度分層：問題難度跨度大，即使單一證明策略無法解決所有問題，也可在特定難度區(qū)間發(fā)揮作用，逐步構(gòu)建多樣化的工具庫

• 標準化平臺：集中式的討論、項目管理和驗證平臺（Lean Zulip、GitHub、Lean），通過貢獻指南和行為準則規(guī)范協(xié)作流程

• 可視化工具：自定義可視化工具幫助參與者獨立識別問題、驗證貢獻，加速項目進展

• 現(xiàn)有工具適配：大量蘊含關(guān)系可直接使用現(xiàn)成自動定理證明器解決，無需過度定制

• 開放接納新技術(shù)：鼓勵參與者提出新想法、技術(shù)和工具，靈活調(diào)整項目方法。

項目關(guān)鍵文檔及重要鏈接

https://teorth.github.io/equational_theories/ 項目入口

https://teorth.github.io/equational_theories/dashboard/ 儀表盤

https://teorth.github.io/equational_theories/blueprint 藍圖

https://teorth.github.io/equational_theories/implications 等式（及蘊含關(guān)系）瀏覽器

https://teorth.github.io/equational_theories/fme 有限原群瀏覽器 FME

https://totallyqed.com/fme/ 有限原群瀏覽器 FME

https://github.com/EricGT/Finite-Magma-Game-Dev 有限原群游戲

https://teorth.github.io/equational_theories/graphiti/ 蘊含關(guān)系可視化工具 Graphiti

https://github.com/teorth/equational_theories/blob/main/paper/contributions.md 矩陣化項目人員分工

https://leanprover.zulipchat.com//channel/458659-Equational Zulipchat頻道

https://www.newton.ac.uk/seminar/46700/ 陶哲軒在艾薩克·牛頓研究所的專題研討會演講 2025-6-10

https://github.com/teorth/equational_theories/wiki/Terence-Tao's-personal-log 陶哲軒個人項目日志

https://terrytao.wordpress.com/2025/12/09/the-equational-theories-project-advancing-collaborative-mathematical-research-at-scale/ 陶哲軒博客對該項目總結(jié)介紹

https://arxiv.org/abs/2512.07087 陶哲軒arxiv論文

其它實用工具：

• 蛋（egg - e-graphs good） - 圖工具 https://egraphs-good.github.io

• MiniZinc——高級約束建模語言 https://www.minizinc.org

• Nauty – 圖自同構(gòu)工具 https://pallini.di.uniroma1.it

• KBCV – Knuth-Bendix 補全可視化器 http://cl-informatik.uibk.ac.at/software/kbcv/

• Instagraph——知識圖譜生成器 https://github.com/yoheinakajima/instagraph

陶哲軒論文目錄供參考https://arxiv.org/abs/2512.07087

參考資料

https://terrytao.wordpress.com/2025/12/09/the-equational-theories-project-advancing-collaborative-mathematical-research-at-scale/

https://arxiv.org/abs/2512.07087

https://teorth.github.io/equational_theories/

https://teorth.github.io/equational_theories/dashboard/

https://teorth.github.io/equational_theories/blueprint

https://teorth.github.io/equational_theories/implications

https://teorth.github.io/equational_theories/fme

https://totallyqed.com/fme/

https://github.com/EricGT/Finite-Magma-Game-Dev

https://teorth.github.io/equational_theories/graphiti/

https://github.com/teorth/equational_theories/blob/main/paper/contributions.md

https://leanprover.zulipchat.com//channel/458659-Equational

https://www.newton.ac.uk/seminar/46700/

https://github.com/teorth/equational_theories/wiki/Terence-Tao's-personal-log

https://arxiv.org/abs/2512.07087

https://egraphs-good.github.io

https://www.minizinc.org

https://pallini.di.uniroma1.it

http://cl-informatik.uibk.ac.at/software/kbcv/

https://github.com/yoheinakajima/instagraph

https://github.com/teorth/equational_theories/wiki/Terence-Tao's-personal-log

小樂數(shù)學(xué)科普近期文章

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉(zhuǎn)載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂加星★

數(shù)學(xué)科普不迷路！