陶哲轩发起的「众包」数学研究项目终于快要迎来胜利时刻！

大约在三周前，陶哲轩提出了一个众包项目，结合专业和业余数学家、自动定理证明器、AI 工具和证明辅助语言 Lean， 来描述与 4694 条 magma（原群） 方程定律相关的蕴含图，这些定律可以使用最多四次 magma 操作调用来表达。也即，需要确定这 4694 条定律之间可能蕴含的的真假。

该项目已运行 19 天，从已解决的原始蕴含的角度来看，该项目（截至撰写本文）已完成 99.9963%：待解决的蕴含中，已被证明为真，已被证明为假，只有悬而未决。尽管在这个集合中，也有蕴含推测为假，但可能很快就正式反驳。

出于编译效率的原因，他们没有在 Lean 中记录这些推测中的每一个证明；只在 Lean 中证明一组较小的蕴含，然后通过传递性来暗示一组更广泛的蕴含（例如，使用以下事实：如果方程 X 蕴含方程 Y，且方程 Y 蕴含方程 Z，则方程 X 蕴含方程 Z）；他们还将很快利用蕴含图的对偶对称性实现进一步简化。

除了感谢众多志愿者为该项目付出的不懈努力，陶哲轩表示现在拥有许多出色的可视化工具来检查（尚未完成的）蕴含图的各个部分。例如，下图描绘了方程 1491：的所有结果，陶哲轩将其昵称为「Oberlix 定律」（它有一个「同伴」——Asterix 定律，即方程 65：）。

下面是正在研究的所有方程定律的表格，以及它们蕴含或被蕴含的定律数量。这些界面也与 Lean 有某种程度的集成：例如，你可以单击来尝试证明 Oberlix 定律蕴含方程 359，；陶哲轩将此留作一个挑战（Lean 中可以进行四行证明）。

过去几周，陶哲轩了解到其中许多定律以前都出现在文献中，并在下图项目中对这些方程进行介绍。例如，除了非常著名的交换律（公式 43）和结合律（公式 4512）之外，一些方程（比如公式 4、公式 29、公式 381、公式 3722 和公式 3744）出现在一些 Putnam 数学竞赛中；公式 168 定义了一个有趣的结构，被称为「中心群」，学者 Evans 和 Knuth 对其进行了研究，并成为 Knuth-Bendix 完成算法的主要灵感来源；公式 1571 对指数为 2 的阿贝尔群进行了分类。

方程汇总地址：https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations

陶哲轩表示 Birkhoff 完备定理起了大作用，如果一个方程定律蕴含另一个，那么可以通过有限次数的重写操作来证明，但是所需要的重写次数可能相当长。上面提到的从 方程 1491 推导出 359 的蕴含已经相当有挑战性，需要重写四五次；从方程 1681 推导出 2 的蕴含非常长。尽管如此，标准自动定理证明器（例如 Vampire）完全能够证明这些蕴含中的绝大多数。

更微妙的是反蕴含，他们必须证明一条定律 X 并不蕴含另一条定律 Y。原则上，他们只需展示一个服从 X 但不服从 Y 的 magma。在很大一部分情况下，他们可以简单地搜索小的有限 magma（例如两个、三个或四个元素的 magma）来获得这种反蕴含。但它们并不总是足够的，事实上，他们知道只有通过构造无限的 magma 才能证明反蕴含。

例如，现在已知「Asterix 定律」并不蕴含「Oberlix 定律」，但所有反例必然是无限的。奇怪的是，已知的构造与集合论中著名的强迫技术有某种相似之处，因为他们不断地将「通用」元素添加到（部分）magma 中， 以强迫存在具有某些特定属性的反例，尽管这里的构造肯定比集合论的构造简单得多。

他们还从交换和非交换环中的「线性」magma 构造中获得了可观的收益，比如与「合流」方程定律相关的自由 magma，以及更普遍的具有完整重写系统的定律。因此，未解决的蕴含数继续稳步减少，不过还没有到宣布该项目胜利的时候。

虽然该项目仍在进行中，但陶哲轩对迄今为止取得的进展感到非常满意，而且对该项目的许多希望已经实现。

在科学方面，他们发现一些新技术和构造，可以证明给定的方程理论并不蕴含另一个方程理论，并且还发现一些奇特的代数结构， 如「Asterix」和「Oberlix」，它们具有有趣的特征。除了此处进行系统搜索之外，其他任何方式都可能无法发现它们。参与者非常多样化，包括各个职业阶段的数学家和计算机科学家、以及感兴趣的学生和业余爱好者。Lean 平台在整合人类生成和机器生成的贡献方面效果很好，后者在是迄今为止最大的贡献来源，但许多自动生成的结果首先由人类在特定情况下获得，然后被泛化和形式化（通常由项目的不同成员完成）。

他们仍在提出许多非正式的数学论证，但它们往往在 Lean 中被迅速形式化，此时关于正确性的争议就会消失，从而专注如何最好地部署各种经过验证的技术来解决剩下的问题。

也许陶哲轩目前唯一期待但尚未看到现代 AI 工具的重大贡献，它们正在以多种次要方式应用于该项目，例如通过 GitHub Copilot 等工具来加速编写 Lean 证明、LaTeX 蓝图和其他软件代码。此外一些可视化工具也主要使用 Claude 等大型语言模型共同编写。

对于解决蕴含这一核心任务，更「老式」的自动定理证明器迄今为止已被证明更为优越。然而，剩余 700 个左右蕴含中的大多数都不适合这些旧工具，尤其涉及 Asterix 和 Oberlix 的蕴含让人类合作者困惑了好几天。所以仍然希望看到现代 AI 在完成剩余蕴含中最难、最顽固的部分发挥更积极的作用。

文章来自于“机器之心“，作者”杜伟“。