陶哲轩原群等式定律——数学家群体合作大项目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小乐

公众号主页

右上角

置顶加星★

数学科普不迷路！