数学「A队」证明了加法和集合之间的关键联系 https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/ Leila Sloman 正是包括两位菲尔兹奖得主在内四位数学家的坚持，才得以证明了一个堪称「加性组 合学圣杯」的猜想，其中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）。 陪集并不具备子群的所有性质，但它又能保留 子群在许多方面的结构。 举个例子，奇数和偶数一样是均匀分布的。 图片 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 个元素，那就意味着和集有k2 /2 个元素。 当 k 很大时（例如1000），k2 /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 的子 群的不超过k1 2 移位而将A 覆盖其中。 这个移位的数量很可能非常大。 但这是一个多 项式，不会随着k 的增加而指数级增长；而如果k 在指数中就会这样。 几天之後，陶哲轩开始形式化证明。 他以协作的方式运行了这个形式化项目，使用了版 本控制软体包GitHub 来协调来自全球25 个志工的贡献。 他们使用了一种名为 Blueprint 的工具。 这个工具是巴黎萨克雷大学数学家Patrick Massot 开发的，可用来 协调组织将陶哲轩所说的「数学式英语」翻译成电脑程式码的工作。 Blueprint 的功能 有很多，其中之一是创建一张图表来描述证明中涉及的各种 逻辑 步骤。 一旦图中所有 气泡都变成陶哲轩所说的「可爱的绿色阴影」，这个团队就算完工了。 对PFR 猜想的证明的依赖图，其中方框是定义，椭圆是定理和引理，全部背景都是绿色说 明该证明已经完全形式化 他们发现论文中存在一些非常小的拼字错误—— 在一条网路讯息中，陶哲轩指出：「这 个计画中与数学最相关的部分的形式化是相对简单直接的，但技术上『显而易见』的步骤 反而耗时最长。 Marton 在她的着名猜想得到证明的几年前去世了，但这个证明帮助彰显了她在熵和 资讯 理论 领域的毕生成就。 「当使用这个熵框架进行研究，而不是我之前尝试的框架时，一 切都好了很多。」Gowers 说，「对我来说，这仍然有些神奇。」 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 114.38.27.129 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1714741523.A.DF4.html