【新智元导读】
AI已完全融入数学家的工作流中。陶哲轩刚刚宣布，最新方程理论项目已完成99.9963%，众包之力外加AI辅助取得了重大成绩。他认为，剩余大约700个让人类头疼的难题，AI或许更有潜力。
AI，已成为菲尔兹奖得主最得心应手的工具。
大约三周前，陶哲轩提出了一个协作项目——
结合专业和业余数学家、自动定理证明器、AI工具，以及证明辅助语言Lean，来描述与4694条幺半群（magmas）方程定理定理相关的蕴含图。
这些定理最多可以使用，四次幺半群运算来表达。
也就是说，需要确定4694条定理之间可能存在4694 * (4694 - 1) = 22028942蕴含的关系真伪。
地址：https://github.com/teorth/equational_theories/blob/main/data/equations.txt
这一项目在9月25日发布当天便启动了，如今，已经紧锣密鼓进行了19天。
刚刚，陶哲轩公布了项目的最新进展：
从已解决原始蕴含关系角度来看，截至目前，项目进度已完成99.9963%。
在需要解决的22028942个蕴含关系中，8178279个被证明为真，13854531个被证明为假，只有826个仍未解决。
而且，项目每一天的进展，他都记录到了个人日志中。
一起看看，陶哲轩如何通过「众包方式」，探索数学新领域。
在集合中，有249个蕴含关系推测为假，并且很快就证明了是假的。
出于编译效率的考量，他们并没有在Lean中记录每一个证明，只在其中证明了一个较小的592790个蕴含关系集合，然后通过传递性推导出更广泛的蕴含关系集合。
例如，利用如果方程X蕴含方程Y，方程Y蕴含方程Z，那么方程X蕴含方程Z的事实。
他们还很快利用蕴含图对偶对称性，对其进一步简化。
经过项目志愿者的不懈努力，陶哲轩称现在有了很多出色的可视化工具（尚未完成的），来检查蕴含图的各个部分。
比如，如下这张图描述了方程1491：x = (y ◇ x) ◇ (y ◇ (y ◇ x ))的所有结果。
陶哲轩将其称之为「Obelix law」。它还有一个伙伴Asterix law，即方程65：x = y ◇ (x ◇ (y ◇ x ))。
如下是，他们正在研究的所有方程定理的表格，以及它们蕴含/被蕴含定理数量。
地址：https://teorth.github.io/equational_theories/implications/
这些界面也在某种程度上与Lean集成。
比如，我们可以点击查看Obelix law蕴含方程359，陶哲轩将其作为题目，让大家进行挑战。他暗示，在Lean中仅用4行就可以完成证明。
在过去的几周里，他还了解到这些定理中，有许多之前已经出现在文献中。
由此，这里编制了这些方程的「导览」。
地址：https://github.com/teorth/equational_theories/wiki/Tour-of-selected-equations
例如，除了众所周知的交换律（方程43）、结合律（方程4512）之外，一些方程（方程14、方程29、方程381、方程3722、方程3744）曾出现在一些Putnam数学竞赛中；
方程168定义了一个引人入胜的结构，被称为「中心幺半群」（central groupoid）。特别是，由Evans和Knuth研究过，并且是Knuth-Bendix完成算法的关键灵感来源；
而方程1571则对指数为二的阿贝尔群（abelian groups）进行了分类。
根据Birkhoff完备性定理，如果一个方程定理蕴含另一个，那么它可以通过有限次重写操作来证明。
不过，所需的重写次数可能相当长。
上面提到的1491蕴含359的证明已经相当具有挑战性，需要四到五次重写。
另外，方程1689蕴含方程2的证明，更是极其冗长。尽管如此，标准的自动定理证明器，如Vampire，完全有能力证明绝大多数这些蕴含关系。
更微妙的是反蕴含关系，在这种情况下必须证明定理X不蕴含定理Y。原则上，只需要展示一个遵循X但不遵循Y的幺半群即可。
在很大一部分情况下，他们可以简单地搜索小型有限幺半群——比如两个、三个或四个元素的幺半群——来获得这种反蕴含关系。
但这些并不足够，事实上，他们只知道有些反蕴含关系，只能通过构造无限幺半群来证明。
比如，现在已知的Asterix law不蕴含Obelix law，但所有反例必然是无限的。
有趣的是，已知的构造方法与集合论中著名的forcing技术有一些相似之处，即不断向（部分）幺半群添加「通用」元素，以forcing存在具有某些特定属性的反例。
不过，这里的构造肯定比集合论构造简单得多。
他们还从「线性」幺半群x ◇ y = ax + by构造中取得了有益的进展。这些构造存在于交换环和非交换环中。
与「汇聚」（confluent）方程定理相关的自由幺半群，以及更普遍的具有完整重写系统的定理。
因此，未解决的蕴含关系数量继续稳步减少。
经过相当繁忙的后端设置和「灭火」（putting out fires）工作后，项目现在运行得相当顺利。
项目在Lean Zulip频道上协调，所有贡献都通过GitHub上的拉取请求（pull request）过程进行，并通过基于问题的GitHub项目进行跟踪。
另外两位维护者Pietro Monticone、Shreyas Srinivas为其提供了宝贵的监督。
与之前的PFR形式化项目相比，这次项目的工作流程遵循了标准的GitHub实践，大致如下：
如果在Zulip讨论过程中，明确需要完成某些特定任务以推进项目（比如，在Lean中形式化讨论线程中已经推导出的蕴含关系证明），就会创建一个「问题」（通常由陶哲轩自己或其他维护者创建），其他贡献者可以「认领」这个问题，单独工作（使用主GitHub仓库的本地副本）。
