打开网易新闻 查看更多图片

新智元报道

编辑:桃子 好困

【新智元导读】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个仍未解决。

打开网易新闻 查看更多图片

而且,项目每一天的进展,他都记录到了个人日志中。

打开网易新闻 查看更多图片

一起看看,陶哲轩如何通过「众包方式」,探索数学新领域。

方程理论项目,进度99.99%

在集合中,有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)方程定理相关的自由幺半群,以及更普遍的具有完整重写系统的定理。

因此,未解决的蕴含关系数量继续稳步减少。

遵循标准GitHub实践,论文很快上线

经过相当繁忙的后端设置和「灭火」(putting out fires)工作后,项目现在运行得相当顺利。

项目在Lean Zulip频道上协调,所有贡献都通过GitHub上的拉取请求(pull request)过程进行,并通过基于问题的GitHub项目进行跟踪。

另外两位维护者Pietro Monticone、Shreyas Srinivas为其提供了宝贵的监督。

与之前的PFR形式化项目相比,这次项目的工作流程遵循了标准的GitHub实践,大致如下:

打开网易新闻 查看更多图片

如果在Zulip讨论过程中,明确需要完成某些特定任务以推进项目(比如,在Lean中形式化讨论线程中已经推导出的蕴含关系证明),就会创建一个「问题」(通常由陶哲轩自己或其他维护者创建),其他贡献者可以「认领」这个问题,单独工作(使用主GitHub仓库的本地副本)。

然后提交「拉取请求」将他们的贡献合并回主仓库。这个请求随后可以由维护者和其他贡献者审查,如果获得批准,就会关闭相关问题。

更广泛地说,他们正努力记录这个设置中的所有过程和经验教训。

这将成为即将发表的关于这个项目的论文的一部分,现正处于初步规划阶段,可能会包括数十位作者。

陶哲轩表示,自己对项目取得的进展非常满意,而且许多最初的期望已经实现。

在科学方面,他们发现了一些新的技术和构造,用来证明一个给定的方程理论不蕴含另一个;他们还发现了一些具有有趣特征的奇特代数结构,如Asterix和Obelix对,是通过系统性搜索方式被发现的。

参与者方面,非常多样化,从各个职业阶段的数学家、计算机科学家,到感兴趣的学生和业余爱好者。

此外,Lean平台在整合人工生成和机器生成的贡献方面表现良好。

机器生成在数量上是迄今为止最大的贡献来源,但许多自动生成往往是基于人类最初在特殊情况下发现的,然后由项目的不同成员进行推广和形式化。

在讨论线程中,他们还进行了许多非正式的数学论证,但这些论证往往会迅速在Lean中形式化,消除了关于正确性的争议就。

进而,研究人员可以转而专注于如何最好地部署各种经过验证的技术,来解决剩余的蕴含关系。

AI并未做出重大贡献

原本,陶哲轩期待看到现代AI工具,能够在项目中做出重大贡献。

但实际上,它们以一种辅助、次要的方式被使用。

比如,通过GitHub Copilot等工具来加速编写Lean证明、LaTeX文档框架、其他软件代码。

此外,他们的几个可视化工具,也主要是使用Claude等大模型共同编写的。

打开网易新闻 查看更多图片

然而,对于解决蕴含关系这一核心任务,更「传统」的自动定理证明器表现更好。

不过,目前剩余的大约700个蕴含关系,大多数不适合使用传统工具来处理。

有几个蕴含关系(特别是涉及Asterix和Obelix那些),已经让人类专家困惑多日。

陶哲轩认为,在解决剩余的、更困难的蕴含关系时,现代AI可能会发挥更重要的作用。

参考资料:

https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/