一队计算机帮助解决了一个已有90年历史的数学问题

一组数学家最终解决了凯勒的猜想，但不是靠他们自己。取而代之的是，他们教会了一队计算机来为他们做这件事。

原始故事经广达杂志许可转载，广达杂志是西蒙斯基金会的一份编辑独立的出版物，其使命是通过报道数学以及物理和生命科学的研究发展和趋势来增强公众对科学的理解。

90年前由奥特-海因里希·凯勒提出的凯勒猜想，是关于用完全相同的瓷砖覆盖空间的问题。它断言，如果用二维正方形瓷砖覆盖二维空间，则至少有两个瓷砖必须共享一条边。它对每个维度的空间都做出了同样的预测--比方说，在使用12维“正方形”瓷砖覆盖12维空间时，你最终将得到至少两个完全相邻的瓷砖。

多年来，数学家们逐渐破解了这一猜想，证明了这一猜想在某些维度是正确的，而在另一些维度是错误的。到今年秋天为止，这个问题只有七维空间还没有解决。

但一种新的计算机生成的证据最终解决了这个问题。去年10月发布在网上的这一证明，是人类的聪明才智与原始的计算能力相结合，可以回答数学中一些最令人烦恼的问题的最新例子。

这项新工作的作者--斯坦福大学的约书亚·布拉肯内克、卡内基梅隆大学的马里恩·海勒和约翰·麦基，以及罗切斯特理工学院的大卫·纳尔韦兹--用40台计算机解决了这个问题。仅仅30分钟后，机器就给出了一个词的答案：是的，这个猜想在七个维度上是正确的。我们也不必把他们的结论建立在信仰上。

答案附带了很长的证据，解释了为什么它是正确的。这一论点过于杂乱无章，人类无法理解，但它可以通过一个单独的计算机程序进行验证，证明是正确的。

换句话说，即使我们不知道计算机做了什么来解决凯勒猜想，我们也可以确信他们做得是正确的。

很容易看出，凯勒的猜想在二维空间是正确的。拿一张纸，试着用相等大小的正方形覆盖它，正方形之间没有缝隙，也没有重叠。你不会走多远就会意识到至少有两个正方形需要共享一条边。如果你周围有块积木，同样很容易看出，这个猜想在三维空间是正确的。1930年，凯勒猜想，这种关系对任何维度的相应空间和瓷砖都成立。

初步结果支持了凯勒的预测。1940年，奥斯卡·佩伦证明了这个猜想在一维到六维空间中是正确的。但50多年后，新一代数学家发现了这一猜想的第一个反例：1992年，杰弗里·拉加里亚斯和彼得·肖尔在10维证明了这一猜想是错误的。

一个简单的论证表明，一旦猜想在一个维度上是错误的，那么它在所有更高的维度上都必然是错误的。因此，在拉加里亚斯和肖尔之后，唯一未确定的维度是7，8和9。2002年，麦基证明了凯勒猜想在8维(因此也在9维)是错误的。

这只留下了维度7的空缺-它要么是猜想成立的最高维度，要么是猜想失败的最低维度。

几十年来，随着数学家们逐渐解决这个问题，他们的方法也发生了变化。佩伦用铅笔和纸计算出了前六个维度，但到了20世纪90年代，研究人员已经学会了如何将凯勒的猜想转化为一种完全不同的形式-一种允许他们将计算机应用于问题的形式。

凯勒猜想的最初表述是关于光滑、连续的空间。在这个空间里，有无限多种放置无限多块瓷砖的方式。但计算机并不擅长解决涉及无限选择的问题--要发挥它们的魔力，它们需要考虑某种离散的、有限的对象。

1990年，Keresztély Corrádi和Sándor Szabó就提出了这样一个离散的物体。他们证明，你可以问与凯勒猜想等价的问题--因此，如果你证明了关于这些物体的某些东西，你必然也证明了凯勒猜想。这有效地将一个关于无穷大的问题简化为一个关于几个数字的算术的更容易的问题。

假设你想解决二维凯勒猜想。科拉迪和萨博想出了一种方法，通过建立他们所谓的凯勒图来实现这一点。

首先，想象桌子上有16个骰子，每个骰子的位置都是有两个点的脸朝上。(它是两个点的事实反映了这样一个事实，即您正在解决第二维的猜想；稍后我们将了解为什么它是16个骰子。)。现在用四种颜色中的任何一种给每个点上色：红色、绿色、白色或黑色。

单个骰子上的点的位置不能互换：可以将一个位置视为表示x坐标，将另一个位置视为表示y坐标。一旦骰子上色，如果两个条件成立，我们将开始在骰子之间画线或边：骰子的一个位置有不同颜色的圆点，在另一个位置，它们的圆点不仅颜色不同，而且成对，红色和绿色形成一对，黑白形成另一对。

因此，例如，如果一个骰子有两个红点，而另一个骰子有两个黑点，则它们不相连：虽然它们满足一个位置的标准(不同颜色)，但它们不符合另一个位置的标准(配对颜色)。但是，如果一个骰子是红黑相间的，而另一个骰子是绿绿相间的，则它们是相连的，因为它们在一个位置有配对的颜色(红-绿)，而在另一个位置有不同的颜色(黑-绿)。

有16种可能的方法可以用四种颜色给两个点上色(这就是为什么我们要用16个骰子)。在你面前排列所有16种可能性。连接所有符合规则的骰子对。现在是关键的问题：你能找到四个彼此相连的骰子吗？

这种完全连接的骰子子集称为集团。如果你能找到一个，你就证明了凯勒猜想在二维空间是错误的。但你不能，因为它不会存在。事实上，没有四个骰子的集团，这意味着凯勒的猜想在二维空间是正确的。

骰子在字面上并不是凯勒猜想中讨论的瓷砖，但你可以认为每个骰子代表一块瓷砖。把分配给点的颜色看作是骰子在空间中的坐标。并将边缘的存在视为两个骰子如何相对于彼此定位的描述。

如果两个骰子具有完全相同的颜色，则它们表示在空间中处于完全相同位置的瓷砖。如果它们没有共同的颜色，也没有配对的颜色(一个骰子是黑白的，另一个是绿红色的)，它们代表的是部分重叠的瓷砖-记住，这在瓷砖中是不允许的。如果两个骰子有一组配对的颜色和一组相同的颜色(一个是红黑的，另一个是绿黑的)，则它们表示共享一个面的瓷砖。

最后，也是最重要的是，如果它们有一组配对的颜色和另一组仅仅是不同的颜色-也就是说，如果它们是由一条边连接的-这意味着骰子代表的是彼此接触但略有偏离的瓷砖，所以它们的脸并不完全对齐。这才是你真正想要调查的情况。由边缘连接的骰子代表没有共享面而连接在一起的瓷砖-这正是推翻凯勒猜想所需的瓷砖排列方式。

“他们需要互相触摸，但他们不能完全接触对方，”Heule说。

30年前，Corrádi和Szabó证明，数学家可以通过调整实验参数，在任何维度使用这个过程来解决凯勒猜想。为了在三维上证明凯勒的猜想，你可以使用216个骰子，在一个面上有三个点，也许还有三对颜色(尽管在这一点上有灵活性)。然后，您将在它们中寻找8个骰子(2³)，它们使用与我们之前使用的相同的两个条件完全连接在一起。

一般说来，为了证明Keller猜想在n维空间中的正确性，你可以使用带有n个点的骰子，试图找到一个大小为2n的集团。你可以认为这个集团代表着一种可以覆盖整个n维空间的“超级瓦片”(由2n个更小的瓦片组成)。

因此，如果你能找到这个超级瓷砖(它本身不包含面部共享瓷砖)，你就可以使用它的翻译或移动的副本来用不共享人脸的瓷砖覆盖整个空间，从而驳斥了凯勒的猜测。

“如果你成功了，你可以通过翻译覆盖整个空间。没有共同面孔的街区将延伸到整个瓷砖。“目前在密歇根大学工作的拉加里亚斯说。

麦基反驳了凯勒在8维的猜想，他找到了256个骰子(28)的集团，所以回答凯勒的7维猜想需要寻找128个骰子(27)的集团。找到那个集团，你就在七维空间证明了凯勒猜想是错误的。另一方面，要证明这样的集团是不可能存在的，那么你就证明了这个猜想是正确的。

不幸的是，找到128个骰子的集团是一个特别棘手的问题。在以前的工作中，研究人员可以利用这样一个事实，即在某种意义上，8维和10维可以被“分解”到更容易处理的低维空间中。这里就没有这么好的运气了。

拉加里亚斯说：“七维是不好的，因为它是质数，这意味着你不能把它分成低维的东西。”“因此，我们别无选择，只能处理这些图表的全部组合。”

对于没有辅助的人脑来说，寻找一个128人的小圈子可能是一项艰巨的任务，但这正是计算机擅长回答的问题-特别是如果你给它一点帮助的话。

要将集团搜索变成计算机可以处理的问题，您需要使用命题逻辑来表示问题。这是一种合并了一组约束的逻辑推理。

假设你和两个朋友正在筹划一个派对。你们三个人正在努力整理嘉宾名单，但你们有一些相互竞争的利益。也许你想邀请艾弗里或者把肯巴排除在外。你的一个合作策划人想邀请肯巴或布拉德，或者两个都邀请。你的另一个合作策划人，别有用心，想把艾弗里或布拉德或者两个人都去掉。考虑到这些限制，你可能会问：有没有一份客人名单能满足所有三位派对策划人的要求？

在计算机科学术语中，这类问题称为可满足性问题。你可以用一个命题公式来描述它，在本例中是这样的，其中字母A，K和B代表潜在的客人：(A Or Not K)and(K Or B)and(Not A Or Not B)and(Not A Or Not B)。

计算机通过为每个变量插入0或1来计算此公式。0表示变量为FALSE或关闭，1表示变量为TRUE或打开。因此，如果你在“A”上填上0，那就意味着艾弗里没有被邀请，而1则表示她被邀请了。有很多方法可以给这个简单的公式分配1和0-或者建立客人列表-在运行它们之后，计算机可能会得出结论，它不可能满足所有相互竞争的需求。不过，在本例中，有两种分配1和0的方法对每个人都有效：A=1，K=1，B=0(表示邀请Avery和Kemba)和A=0，K=0，B=1(表示只邀请Brad)。

像这样求解命题逻辑语句的计算机程序称为SAT求解器，其中“SAT”代表“可满足性”。它探索变量的每一个组合，并产生一个词的答案：要么是，有满足公式的方法，要么是没有，没有。

匹兹堡大学(University Of Pittsburgh)的托马斯·黑尔斯(Thomas Hales)说：“你只需决定每个变量的真假，就能使整个公式为真，如果你能做到这一点，公式就是令人满意的，如果你做不到，公式就是不能满足的，”匹兹堡大学的托马斯·黑尔斯(Thomas Hales)说。

是否有可能找到一个规模为128的集团的问题也是类似的问题。它也可以写成命题公式并插入到SAT解算器中。从大量的骰子开始，每个骰子有七个点和六种可能的颜色。你能给这些点上色，这样128个骰子就可以按照规定的规则连接在一起了吗？换句话说，有没有一种分配颜色的方法可以让这个集团成为可能？

抓住这个关于集团的问题的命题公式相当长，包含39,000个不同的变量。每个值都可以分配到两个值(0或1)中的一个。因此，变量的可能排列，或骰子上排列颜色的方式的数量是23万9千个-这是一个非常非常大的数字。

为了回答凯勒关于七维空间的猜想，计算机必须检查每一种组合-要么全部排除(意味着不存在128个大小的集团，而凯勒在第七维空间是真的)，要么只找到一个可行的(意味着凯勒是假的)。

麦基说：“如果你用一台幼稚的电脑检查所有可能的[配置]，那就是这个324位数的病例数。”这将需要世界上最快的计算机，直到时间的尽头，他们才会用尽所有的可能性。

但这项新工作的作者们想出了计算机如何在不实际检查每种可能性的情况下得出明确的结论。效率是关键。

麦基回忆起，在他看来，这个项目真正走到了一起的那一天。他正站在卡内基梅隆大学(Carnegie Mellon University)办公室的一块黑板前，与他的两位合著者希勒(Heule)和布拉基内克(Brakensek)讨论这个问题，这时希勒提出了一种组织搜索的方法，以便在合理的时间内完成搜索。

麦基说：“那天我的办公室里有真正的智力天才在工作。”“这就像在看韦恩·格雷茨基，就像在NBA总决赛中看勒布朗·詹姆斯。我现在(光是想一想)就起鸡皮疙瘩了。“。

有很多方法可以帮助您搜索特定的凯勒图。假设你在一张桌子上放了很多骰子，你想要安排其中的128个骰子，使其符合凯勒图的规则。也许你安排对了其中的12个，但是你找不到添加下一个骰子的方法。在这一点上，您可以排除所有128个骰子的配置，这些配置涉及12块不可行的起始配置。

目前在麻省理工学院工作的肖尔说：“如果你知道你分配的前五件事不匹配，你就不必考虑其他任何变量，这通常会大大减少搜索的工作量。”

另一种形式的效率涉及对称性。当物体对称时，我们认为它们在某种意义上是相同的。这种相同之处让你只需研究物体的一部分就能理解整个物体：瞥见半个人的脸，你就可以重建整个脸部。

类似的快捷方式也适用于凯勒图。再想象一下，你正在桌子上安排骰子。也许您可以从桌子的中心开始，然后在左侧构建一个配置。你掷了四个骰子，然后撞上了路障。现在，您已经排除了一个起始配置-以及基于它的所有配置。但您也可以排除开始配置的镜像-当您以相同的方式放置骰子，但向右构建时，您得到的骰子的排列方式。

黑尔斯说：“如果你能找到一种方法来解决可满足性问题，并以一种智能的方式考虑到对称性，那么你就会让问题变得容易得多。”

这四位合作者以一种新的方式利用了这种搜索效率-特别是，他们自动考虑了关于对称性的问题，以前的工作依赖于数学家实际手工处理它们。

他们最终简化了对128个小集团的搜索，因此他们的SAT解算器只需搜索约10亿(230)个配置，而不是检查23.9万个配置。这将可能耗费亿万年的搜索变成了早晨的琐事。最后，仅仅经过半个小时的计算，他们就有了答案。

“电脑说没有，所以我们知道这个猜想是成立的，”海勒说。没有办法给128个骰子上色，使它们彼此相连，所以凯勒的猜想在第七维是正确的：任何覆盖空间的瓷砖排列不可避免地包括至少两个共用一张脸的瓷砖。

计算机实际上提供的不仅仅是一个词的答案。他们用200 GB大小的长长的证据来支持这一观点，证明了他们的结论是正确的。

证明远不止是计算机检查的所有变量配置的读数。这是一个合乎逻辑的论点，它确立了想要的派系不可能存在。这四名研究人员将凯勒的证明输入一个正式的验证器-一个追踪论点逻辑的计算机程序-并确认它是有效的。

麦基说：“你不会简单地检查所有的案件，什么也找不到，你检查了所有的案件，你能够写出一个证据，证明这个东西不存在。”“你可以写一份不可满足性的证明。”

最初的故事经广达杂志许可转载，广达杂志是西蒙斯基金会的一份编辑独立的出版物，其使命是通过报道数学、物理和生命科学的研究发展和趋势来加强公众对科学的理解。

🎙️收听“连线”，这是我们关于未来如何实现的新播客。收看最新剧集，订阅📩时事通讯，跟上我们所有节目的最新动态。

💻使用我们Gear团队最喜欢的笔记本电脑、键盘、替代打字设备和降噪耳机升级您的工作游戏