陶哲軒原群等式定律——數學家群體合作大項目440天基本收官，就差臨門一腳！

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

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

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

該項目為未來更多的大規模數學家社區合作項目提供了優秀示范。

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

譯者：zzllrr小樂（數學科普公眾號）2025-12-10

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

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

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

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

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

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

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

• 猜測定律的完整重寫系統（如 E3523 的重寫系統）

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

該項目成功的借鑒意義

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

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

+形式驗證（Lean）

+現代項目管理工具（Github）

+數據可視化工具（Graphviz + 自制工具）

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

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

+社區標準（大多用 CONTRIBUTING.md 來規范）

在最終論文中，陶哲軒總結出該項目成功的關鍵因素：

• 目標明確：核心目標清晰，有明確的結束條件和量化進度指標，引導參與者聚焦關鍵任務

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

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

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

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

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

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

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

項目關鍵文檔及重要鏈接

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 有限原群瀏覽器 FME

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

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

https://teorth.github.io/equational_theories/graphiti/ 蘊含關系可視化工具 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/ 陶哲軒博客對該項目總結介紹

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

其它實用工具：

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

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

• Nauty – 圖自同構工具 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

小樂數學科普近期文章

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

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

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

收藏、分享、轉載、投稿

查看原始文章出處

點擊zzllrr小樂

公眾號主頁

右上角

置頂加星★

數學科普不迷路！