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

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

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

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

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

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

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

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

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

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

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

• 輔助編寫(xiě)圖形用戶界面代碼；

• 提供代碼自動(dòng)補(bǔ)全（如 GitHub Copilot）

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

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

該項(xiàng)目成功的借鑒意義

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

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

+形式驗(yàn)證（Lean）

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

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

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

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

+社區(qū)標(biāo)準(zhǔn)（大多用 CONTRIBUTING.md 來(lái)規(guī)范）

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

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

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

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

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

• 標(biāo)準(zhǔn)化平臺(tái)：集中式的討論、項(xiàng)目管理和驗(yàn)證平臺(tái)（Lean Zulip、GitHub、Lean），通過(guò)貢獻(xiàn)指南和行為準(zhǔn)則規(guī)范協(xié)作流程

• 可視化工具：自定義可視化工具幫助參與者獨(dú)立識(shí)別問(wèn)題、驗(yàn)證貢獻(xiàn)，加速項(xiàng)目進(jìn)展

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

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

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

https://teorth.github.io/equational_theories/ 項(xiàng)目入口

https://teorth.github.io/equational_theories/dashboard/ 儀表盤(pán)

https://teorth.github.io/equational_theories/blueprint 藍(lán)圖

https://teorth.github.io/equational_theories/implications 等式（及蘊(yùn)含關(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/ 蘊(yùn)含關(guān)系可視化工具 Graphiti

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

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

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

https://github.com/teorth/equational_theories/wiki/Terence-Tao's-personal-log 陶哲軒個(gè)人項(xiàng)目日志

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

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

其它實(shí)用工具：

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

• MiniZinc——高級(jí)約束建模語(yǔ)言 https://www.minizinc.org

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

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

• Instagraph——知識(shí)圖譜生成器 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

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

·開(kāi)放 · 友好 · 多元 · 普適 · 守拙·

讓數(shù)學(xué)

更加

易學(xué)易練

易教易研

易賞易玩

易見(jiàn)易得

易傳易及

歡迎評(píng)論、點(diǎn)贊、在看、在聽(tīng)

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

查看原始文章出處

點(diǎn)擊zzllrr小樂(lè)

公眾號(hào)主頁(yè)

右上角

置頂加星★

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