“子群”陶哲轩用 AI 形式化的证明究竟是什么？一文看懂 PFR 猜想的前世今生

2023-12-10 15:05:12来源：机器之心Pro

今天，很高兴为大家分享来自机器之心Pro的陶哲轩用 AI 形式化的证明究竟是什么？一文看懂 PFR 猜想的前世今生，如果您对陶哲轩用 AI 形式化的证明究竟是什么？一文看懂 PFR 猜想的前世今生感兴趣，请往下看。

机器之心编译

编辑：panda

正是包括两位菲尔兹奖获得者在内四位数学家的坚持，才得以证明了一个堪称「加性组合学圣杯」的猜想，其中 AI 辅助证明起到了不可磨灭的作用。

12 月 5 日，著名数学家、菲尔兹奖获得者陶哲轩在社交网络宣布：对多项式 Freiman-Ruzsa 猜想（PFR）的证明进行形式化的 Lean4 项目成功完成，并且耗时仅三周时间，其依赖图的全部节点都带上了「可爱的绿色阴影」。

Lean 编译器也报告该猜想符合标准公理，可以说这是计算机和 AI 辅助证明的一项巨大成功。

但多项式 Freiman-Ruzsa 猜想究竟是什么？为什么对该猜想的证明不仅是一个数学问题，而且对计算机科学也很重要？量子杂志近日报道了这项成就不凡的数学证明及其令人惊叹的形式化工作，并在文中对多项式 Freiman-Ruzsa 猜想的提出和证明历程进行了梳理与科普。

总结起来：四位著名数学家（包括两位菲尔兹奖获得者）证明了一个堪称「加性组合学圣杯」的猜想。在一个月的时间内，陶哲轩领导的一个松散的合作团队通过计算机辅助证明进行了验证。

下面就进入他们的故事吧。

在一个随机选取的数值集合中，加法可能会如野火蔓延，势不可挡。

对于这样一个集合，如果将其中每两个数加起来，就会得到一个新的列表并且其中所含的数值将远远多于一开始的集合。如果一开始的集合有 10 个随机数，那么新的列表（称为和集）会有大约 50 个元素。如果一开始是 100 个随机数，那么和集中可能会有大约 5000 个元素；而如果初始有 1000 个数，那么和集会有 50 万个数。

但如果初始集合有结构，则和集中的数会少得多。假设有另一个包含 10 个数的集合：这些数都是 2 到 20 之间的偶数。由于不同的一对数可能会得到相同的求和结果（比如 10+12=8+14=6+16），因此和集只会有 19 个数，而非 50 个。当初始集合变得越来越大时，这一差异也会越来越显著。一个由 1000 个数构成的结构化列表的和集可能仅会有 2000 个数。

1960 年代，数学家 Gregory Freiman 开始研究和集较小的集合，以探究加法和集合结构之间的联系 —— 这是定义加性组合学（additive combinatorics）这一数学领域的一个关键联系。Freiman 取得了出色的进展，他证明：一个和集较小的集合必然被包含在一个更大的集合内并且这个更大集合的元素具有高度规则的模式。但自那以后，这一领域就停滞不前了。「Freiman 最初的证明非常难以理解，以至于没人能真正确定它到底是不是正确的。因此它没有产生应有的影响。」法兰西公学院和剑桥大学的数学家 Timothy Gowers 说，他也是一位菲尔兹奖获得者，「但后来 Imre Ruzsa 突然出现了。」

Ruzsa 在 1990 年代通过两篇论文用一套优雅的新论证重新证明了 Freiman 定理。几年之后，一位颇具影响力的匈牙利数学家 Katalin Marton（已于 2019 年去世）探究了一个问题：小的和集能够揭示出原始集合的结构的哪些方面？她替换了该集合中出现的元素的类型与数学家应当找寻的结构的类型，并认为这能让数学家提取出更多信息。Marton 的猜想与证明系统、编码理沦和密码学存在关联，并且在加性组合学领域具有崇高的地位。

她的猜想「感觉是我们之前无法理解的最基本的东西之一。」牛津大学数学家 Ben Green 说，「它就是我关心的很多事情的基础。」

Green 与 Gowers、加利福尼亚大学圣迭戈分校的 Freddie Manners 以及加利福尼亚大学洛杉矶分校的一位菲尔兹奖获得者陶哲轩（Terence Tao）组成了一个团队。以色列数学家和博主 Gil Kalai 将其称为 A-team，也即数学家精英团队。他们在 11 月 9 日发布的论文《On a conjecture of Marton》中证明了该猜想的一个版本。

论文地址：https://arxiv.org/pdf/2311.05762.pdf

未参与该研究的莱斯大学数学家 Nets Katz 描述说这份证明「简单直接得堪称美丽」，并且「多少算是完全出乎意料」。

然后陶哲轩开始通过 Lean 来形式化该证明。Lean 是一种可帮助数学家验证定理的编程语言。不过几周时间，他就成功完成了。12 月 5 日星期二一早，陶哲轩宣布 Lean 已经完成对该猜想的证明，并且没有任何 sorry。sorry 是 Lean 中一个标准陈述，表示计算机无法验证某个特定步骤。这是自 2021 年以来这样的证明工具最亮眼的成就，并成为了数学家编写证明的方式的转折点，也就是开始以计算机能理解的方式编写证明。Gowers 说：如果这些工具变得很容易，能让数学家轻松使用，那么它们就可能替代往往耗时漫长且繁重艰巨的同行评审过程。

这一证明的组分已经酝酿了数十年时间。Gowers 在 2000 年代构想了它的前几步。但还要另外 20 年，Kalai 所称的领域「圣杯」才得以证明。

群

为了理解 Marton 猜想，熟悉群（group）的概念会很有帮助。简单来说，群是由集合和运算构成的数学对象。这里我们假设有整数集（一个包含无限个数的集合）和加法运算。我们每次将两个整数相加，便会得到另一个整数。加法也服从其它一些群运算规则，比如结合律，也就是可以交换运算的顺序：3 + (5 + 2) = (3 + 5) + 2.

在一个群内，你有时候可以找到满足该群所有性质的较小集合。举个例子，任意两个偶数相加会得到另一个偶数。偶数本身就是一个群，这让其成为了整数的子群（subgroup）。而奇数却不一样，它并非一个子群。如果你将两个奇数加到一起，则会得到一个偶数 —— 这不在原来的集合中。但只需让每个偶数都加 1，便能得到所有奇数。像这样的有移位（shift）的子群称为陪集（coset）。陪集并不具备子群的所有性质，但它又能保留子群在许多方面的的结构。举个例子，奇数和偶数一样是均匀分布的。

Timothy Gowers

Marton 猜想如果有一个由群元素组成的集合 A，其和集并不比 A 本身大很多，那么就会存在某个具有一个特殊性质的子群 G。对 G 执行几次移位可以得到一些陪集，而这些陪集组合起来就会包含原始集合 A。此外，她认为陪集的数量并不会比和集的大小增长更快 —— 她相信这应该是一个多项式关系，而非远远更快的指数级增长。

这个研究方向听起来可能好像就是为了满足好奇心，似乎没什么实际用途。但由于它和一个了解子群的总体结构的简单测试（将集合中的两个元素加起来会发生什么？）有关，所以对数学家和计算机科学家来说就非常重要了。当计算机科学家想要使得加密消息一次只能被解码一部分时，也会遇到这个想法的广义版本。它也会出现在概率可检验证明（probabilistically checkable proof）中 —— 这种证明形式让计算机科学家可以通过检验少量孤立的信息来执行验证。

对于上述的每种情况，你只需要研究一个结构中的一些点，就能得出与一个更大更高层结构有关的结论；比如只需解码一个长消息中的少量比特或验证一个复杂证明的一小部分。

牛津大学的 Tom Sanders（他以前是 Gowers 的学生，现在是 Gowers 的同事）说：「你要么可以假设一切都是一个群的一个大子集，要么可以从许多附加巧合的存在中得到你想要的一切。这两种观点都很有用。」

Ruzsa 在 1999 年发表了 Marton 猜想，并充分说明了她的贡献和成就。「她独立于我和 Freiman 得出了这个猜想，而且可能先于我们。」他说，「也因此，在我和她交谈过之后，我决定用她的名字来命名这个猜想。」尽管如此，数学家现在还是将其称为多项式 Freiman-Ruzsa 猜想，简称 PFR。

零和一

和许多数学对象一样，群也有很多不同的形式。Marton 猜测她的猜想对所有群都成立。这一点还有待证明。这篇新论文证明其对某一特定类型的群成立，这类群的元素是 (0, 1, 1, 1, 0) 这样的二进制数列表。由于计算机的工作过程就基于二进制，因此这个群对计算机科学至关重要。但它也对加性组合学很有用。「它就像是一个玩具设置，你可以在其中玩耍，尝试各种东西。」Sanders 说，「这里的代数操作起来比非负整数（whole number）容易太多了。」

这些列表的长度是固定的，而且每一位都要么为 0，要么为 1。这样的两个列表相加就是将一个列表的每一项与另一列表的对应项相加，规则包括 1 + 1 = 0。那么 (0, 1, 1, 1, 0) + (1, 1, 1, 1, 1) = (1, 0, 0, 0, 1)。PFR 试图搞清楚：如果一个集合算不上是子群，但具有某些类似群的特征，那么这个集合看起来会是什么样。

为了更清楚地说明 PFR，请想象一下你有一个二元列表构成的集合 A。现在从 A 中取出每一对元素并相加。所得到的和可构成 A 的和集，记为 A+A。如果 A 中的元素是随机选取的，那么大部分的和都彼此不同。如果 A 有 k 个元素，那就意味着和集有 k²/2 个元素。当 k 很大时（比如 1000），k²/2 就会比 k 大很多。但如果 A 是一个子群，那么 A+A 的每个元素都在 A 中，这就意味着 A+A 的大小和 A 本身是一样的。

PFR 考虑的集合不是随机的，但也不是子群。在这些集合中，A+A 的元素数量会有些小，比如 1 万或 10 万。加利福尼亚大学圣迭戈分校的计算机科学家 Shachar Lovett 说：「当你的结构概念比仅仅作为精确的代数结构丰富得多时，这真的会很有用。」

就数学家所知，所有服从这一性质的集合「都相当接近于真正的子群。」陶哲轩说，「这是一个直觉认识，也就是没有其它类型的假群存在。」Freiman 在其原研究成果中证明了这一命题的一个版本。1999 年时，Ruzsa 将 Freiman 定理从整数扩展到了二元列表设置。他证明，当 A+A 的元素数量是 A 的大小的常数倍时，A 必定被包含在一个子群内。

但 Ruzsa 定理需要子群非常巨大才行。Marton 的见解是假定 A 不是包含在一个巨大的子群中，而是可以包含在一个子群的多项式数量的陪集中并且这个子集不大于原始集合 A。

好想法看一眼就知道

千年之交那段时间，Gowers 在研究与包含均匀相间的字符串的集合相关的另一问题时看到了 Ruzsa 对 Freiman 定理的证明。「我就需要这样的东西，差不多就是从有关一个特定集合的松散得多的信息中获取结构化信息。」Gowers 说，「我非常幸运，就在那不久前，Ruzsa 刚给出这个美不胜收的证明。」

Gowers 开始着手尝试证明该猜想的多项式版本。他的想法是先从和集相对较小的集合 A 开始，然后逐渐操作 A，将其变成一个子群。如果他能证明所得子群与原始集合 A 相似，他就可以轻松断定这个猜想是正确的。Gowers 将这个想法分享给了自己的同事，但没人能将其转化成完整的证明。尽管 Gowers 的策略能成功处理一些情况，但在其它情况中，这种操作却会让 A 更加远离多项式 Freiman-Ruzsa 猜想的预期结论。

最终，该领域放弃了这一思路。2012 年，Sanders 几乎证明了 PFR。但他需要的移位子群的数量高于多项式水平，尽管只高一点点。Gowers 说，「一旦他做到了，就意味着这事件变得不那么紧迫了，但这仍然是一个我非常喜欢的好问题。」

但 Gowers 的想法依然留存在他同事的记忆和硬盘中。「那是一个真正的好想法。」Green 说，他也曾是 Gowers 的学生，「好想法看一眼就知道。」今年夏季，Green、Manners 和陶哲轩终于将 Gowers 的想法从炼狱中解放了出来。

在决定研究已有 20 年历史的 Gowers 想法之前，Green、陶哲轩和 Manners 的合作成果已经可以罗列 37 页之长。在 6 月 23 日的论文《Sumsets and entropy revisited》中，他们成功使用了概率论中的「随机变量」概念来探测具有小和集的集合的结构。通过这种切换，该团队可以更巧妙地操作集合。「处理随机变量在某种程度上比处理集合要简单得多。」Manners 说，「对于随机变量，我可以稍微调整其中一个概率，而这就可能会给我一个更好的随机变量。」

从这个概率角度入手，Green、Manners 和陶哲轩可以不用再面对一个集合的元素数量，而是可以去衡量一个随机变量中所包含的信息，这个量被称为熵（entropy）。对加性组合学来说，熵并不是新东西。事实上，陶哲轩在 2000 年代末就尝试过推广这一概念。但还没有人试过将其用于多项式 Freiman-Ruzsa 猜想。Green、Manners 和陶哲轩发现它很强。但他们仍然不能证明该猜想。

当这个研究团队仔细研究他们的新成果时，他们意识到终于建立了一个可让 Gowers 那蛰伏的想法重获新生的环境。如果使用集合的熵来衡量集合的大小，而不是元素数量，则其技术细节可能会好处理得多。「某一时刻我们意识到，比起我们当时正在尝试的思路，这些来自 Tim 的 20 年前的旧想法实际上更可能有效。」陶哲轩说，「于是我们把 Tim 带回了这个项目。然后所有的碎片都出人意料地很好地拼合在了一起。」

尽管如此，在给出完整的证明前，还有很多细节要处理。「我们四个人都还各自忙着其它事，这是有点愚蠢的。」Manners 说，「你希望发表这个伟大的结果并且告诉全世界，但你实际上还依然必须要去写期中报告。」最终，这个团队坚持了下来，并于 11 月 9 日发表了论文。他们证明，如果 A+A 不大于 A 的大小的 k 倍，那么可通过一个不大于 A 的子群的不超过 k¹² 移位而将 A 覆盖其中。这个移位的数量很可能非常大。但这是一个多项式，不会随 k 的增大而指数级增长；而如果 k 在指数中就会这样。

几天之后，陶哲轩开始形式化该证明。他以协作的方式运行了这个形式化项目，使用了版本控制软件包 GitHub 来协调来自全球 25 个志愿者的贡献。他们使用了一种名为 Blueprint 的工具。这个工具是巴黎萨克雷大学数学家 Patrick Massot 开发的，可用于协调组织将陶哲轩所说的「数学式英语」翻译成计算机代码的工作。Blueprint 的功能有很多，其中之一是创建一张图表来描述证明中涉及的各种逻辑步骤。一旦图中所有气泡都变成陶哲轩所说的「可爱的绿色阴影」，这个团队就算完工了。