一群数学家终于完成了凯勒的猜想，但没有自己解决。取而代之的是，他们教了一批计算机来为他们做。
奥特·海因里希·凯勒（Ott-Heinrich Keller）于90年前提出了凯勒的猜想，这是用相同的瓷砖覆盖空间的问题。它断言，如果用二维正方形瓷砖覆盖二维空间，则至少两个瓷砖必须共享一条边。它对每个维度的空间都做出了相同的预测-在使用12维“正方形”图块覆盖例如12维空间时，您将最终得到至少两个彼此精确邻接的图块。
多年以来，数学家们逐渐摒弃了这一猜想，证明它在某些方面是正确的，而在另一些方面是错误的。截至今年秋天，仅对七维空间这个问题仍未解决。
但是新的计算机生成的证明终于解决了这个问题。该证明于去年10月在线发布，是人类独创性结合原始计算能力如何解决数学中一些最棘手的问题的最新示例。
新作的作者- 约书亚Brakensiek斯坦福大学，Marijn Heule和约翰·麦基卡内基-梅隆大学的，和大卫NARVAEZ罗切斯特技术研究所-解决了使用40台电脑的问题。仅仅30分钟后，机器就给出了一个单词的答案：是的，这个猜想在七个维度上都是正确的。而且我们不必就信仰得出结论。
答案附有很长的证明，解释了为什么是正确的。该论点过于笼统，无法为人类所理解，但可以通过单独的计算机程序验证其正确性。
换句话说，即使我们不知道计算机如何解决凯勒的猜想，我们也可以向自己保证他们正确地做到了。
神秘的第七维度
不难发现，凯勒的猜想在二维空间中是正确的。取一张纸，并尝试用相等大小的正方形覆盖它，正方形之间没有间隙且没有重叠。在意识到至少两个正方形需要共享一条边之前，您不会走得太远。如果周围有块，则很容易看到该猜想在三维空间中是正确的。在1930年，凯勒（Keller）推测这种关系适用于任何尺寸的相应空间和瓷砖。
早期结果支持凯勒的预测。1940年，奥斯卡·佩隆（Oskar Perron）证明了猜想对于尺寸为1到6的空间是正确的。但是50多年后，新一代数学家找到了该猜想的第一个反例：Jeffrey Lagarias和Peter Shor在1992年证明了该猜想在10维上是错误的。
插图显示如何用正方形平铺2D平面或使用立方体平铺3D空间不可避免地导致某些形状完美共享边
一个简单的论证表明，一旦猜想在一个维度上为假，那么在所有更高维度上就必然为假。因此，在拉加里亚斯和索尔之后，唯一未解决的维度是7、8和9。2002年，麦基证明了凯勒的猜想在第8维（因此在第9维）也是错误的。
剩下的只是维度7，它是猜想所在的最高维度，或者是失败的最低维度。
Heule说：“没人确切知道那里发生了什么。”
将点连接
几十年来，随着数学家们逐渐解决这一问题，他们的方法发生了变化。Perron用铅笔和纸算出了前六个维度，但是到1990年代，研究人员已经学会了如何将Keller的猜想转换成完全不同的形式-一种使他们可以将计算机应用于问题的形式。
凯勒猜想的最初表述是光滑，连续的空间。在该空间内，有无数种方法来放置无限多的图块。但是计算机并不擅长解决涉及无限选择的问题-要发挥其魔力，他们需要某种离散的，有限的对象来思考。
Marijn Heule的一件蓝色衬衫，坐在一个白色的房间里的照片
卡内基梅隆大学的Marijn Heule帮助设计了凯勒猜想在第7维的证明。
看的习惯
1990年，KeresztélyCorrádi和SándorSzabó提出了一个如此离散的对象。他们证明了您可以提出与凯勒猜想等效的关于该对象的问题，因此，如果您对这些对象进行证明，则也必须证明凯勒的猜想。这有效地将无穷大的问题简化为几个数的算术的简单问题。
运作方式如下。
假设您想解决二维的凯勒猜想。Corrádi和Szabó提出了一种建立所谓的Keller图的方法。
首先，想象一下桌上有16个骰子，每个骰子的位置都使两个点的面朝上。（它是两个点的事实反映了您正在解决第二维的猜想的事实；我们马上就会知道为什么它是16个骰子。）现在使用四种颜色（红色，绿色，白色或红色）为每个点着色黑色。
单个骰子上点的位置不可互换：将一个位置表示为x坐标，将另一个位置表示为y坐标。骰子着色后，如果满足以下两个条件，我们将开始在成对骰子之间绘制线条或边缘：骰子在一个位置具有不同颜色的点，在另一个位置具有不仅仅颜色的点不同但成对，红色和绿色形成一对，黑色和白色形成一对。
插图显示了二维的Keller图，骰子上带有不同色点的骰子，以及四个完全相连的骰子的理论集团看起来（如果存在）
因此，例如，如果一个骰子有两个红点，而另一个骰子有两个黑点，则它们没有连接：虽然它们满足一个位置的标准（不同的颜色），但不满足另一个位置的标准（配对的颜色）。但是，如果一个管芯被染成红黑色，而另一个管芯被染成绿绿色，则它们是相连的，因为它们在一个位置具有成对的颜色（红绿色），而在另一位置具有不同的颜色（黑绿色）。
使用四种颜色为两个点着色的方法有16种（这就是为什么我们要使用16个骰子的原因）。将所有16种可能性排列在您面前。连接所有符合规则的骰子。现在来解决关键问题：您能否找到四个相互连接的骰子？
这样完全相连的骰子子集称为集团。如果找到一个，就证明凯勒的猜想在第二维上是错误的。但是您不能，因为它不存在。没有四个骰子集团的事实意味着凯勒的猜想在第二维度上是正确的。
骰子从字面上看并不是凯勒猜想中要讨论的瓷砖，但您可以将每个骰子视为代表一个瓷砖。将分配给点的颜色视为位于骰子在空间中的坐标。并将边缘的存在视为两个骰子如何相对放置的描述。
如果两个骰子具有完全相同的颜色，则它们表示在空间中处于完全相同位置的图块。如果它们没有共同的颜色，也没有成对的颜色（一个骰子是黑白，另一个是绿红色），则它们表示部分重叠的图块-记住，不允许在图块中使用。如果两个骰子具有一组成对的颜色，而一组骰子具有相同的颜色（一组为红黑色，另一组为绿黑色），则它们表示共享一个面的图块。
最后，最重要的是，如果它们具有一组成对的颜色，而另一组颜色仅是不同的-也就是说，如果它们通过一条边连接，则表示骰子代表彼此触摸但发生了位移的小块彼此稍微分开，以使他们的脸不完全对齐。这是您真正要调查的条件。通过边连接的骰子表示未共享面就连接的图块-恰好是证明凯勒猜想所需的一种排列方式。
休尔说：“他们需要相互触摸，但不能完全相互触摸。”
图示说明了Keller图中不同骰子与图块的等效配置之间的关系
扩大
30年前，Corrádi和Szabó证明了数学家可以通过调整实验参数，使用此程序来解决凯勒在任何维度上的猜想。为了在三个维度上证明凯勒的猜想，您可以使用216个骰子，在脸上带有三个点，并可能使用三对颜色（尽管这一点很灵活）。然后，您将寻找八个骰子（23 ），它们之间使用我们之前使用的相同两个条件相互完全连接。
作为一般规则，要证明维度为n的凯勒猜想，请使用带有n个点的骰子，并尝试找到大小为2 n的集团。您可以认为这个集团代表了一种“超级图块”（由2 n个较小的图块组成），可以覆盖整个n维空间。
因此，如果您可以找到此超级图块（它本身不包含任何人脸共享图块），则可以使用其平移或移位副本使用不共享人脸的图块覆盖整​​个空间，从而反驳了Keller的猜想。
“如果成功，您可以通过翻译覆盖整个领域。没有共同面孔的街区将延伸到整个地砖。
那天我办公室里工作的是真正的智力天才。就像看韦恩·格雷茨基，就像看NBA总决赛中的勒布朗·詹姆斯一样。
卡内基梅隆大学John Mackey
麦基通过找到256个骰子（2 8）的集团来反驳凯勒在八度的猜想，因此要回答七维的凯勒的猜想就需要寻找128个骰子（2 7）的集团。找到那个集团，您就证明了凯勒的猜想在第七维度上是错误的。另一方面，证明这样的集团是不存在的，并且您已经证明了这种猜想是正确的。
不幸的是，找到128个骰子团是一个特别棘手的问题。在以前的工作中，研究人员可以利用以下事实：从某种意义上说，可以将维度8和10“分解”为更易于使用的较低维度的空间。这里没有这种运气。
Lagarias说：“第七维不好，因为它是质数，这意味着您不能将其分解为低维事物。” “因此，别无选择，只能处理这些图的全部组合。”
对于无助的人脑来说，寻找大小为128的小队可能是一项艰巨的任务，但这恰恰是一台计算机擅长回答的问题，尤其是在您需要一点帮助的情况下。
逻辑语言
要将对派系的搜索变成计算机可以解决的问题，您需要使用命题逻辑来表示问题。这是一种逻辑推理，其中包含一组约束。
假设您和两个朋友正在计划一个聚会。你们三个人试图将来宾列表放在一起，但是您有一些竞争的利益。也许您想邀请Avery或排除Kemba。您的一位共同计划者想邀请Kemba或Brad或他们两者都邀请。您的另一位共同计划者要用斧头打磨，想离开Avery或Brad或他们俩。鉴于这些限制，您可能会问：是否有一个满足所有三方计划者的客人名单？
用计算机科学的术语来说，这类问题被称为可​​满足性问题。您可以通过在这种情况下看起来像这样的命题公式中描述它来解决它，其中字母A，K和B代表潜在客人：（A OR NOT K）AND（K OR B）AND（NOT A是否B）。
计算机通过为每个变量插入0或1来评估此公式。0表示变量为false或已关闭，而1表示变量为true或已打开。因此，如果您为“ A”输入0，则表示不邀请Avery，而为1则表示邀请她。有很多方法可以为这个简单的公式分配1和0（或建立来宾列表），并且在运行它们后计算机可能会得出结论，无法满足所有竞争需求。但是，在这种情况下，有两种分配给所有人的1和0的方法：A = 1，K = 1，B = 0（意味着邀请Avery和Kemba），A = 0，K = 0，B = 1 （意味着只邀请布拉德）。
像这样解决命题逻辑语句的计算机程序称为SAT求解器，其中“ SAT”代表“可满足性”。它探索变量的每种组合并产生一个单词的答案：是的，有一种方法可以满足公式，否则的话，没有。
约翰·麦基（John Mackey）穿着白衬衫在黑板前的照片
卡内基梅隆大学的约翰·麦克基生动地回忆起他办公室里的一天，他的团队想出了一种方法，使计算机可以解决凯勒的猜想。
CMU Jocelyn Duffy
大学的托马斯·海尔斯（Thomas Hales）表示：“您只需以使整个公式为真的方式确定每个变量是对还是错，就可以做到，满足条件，就不能满足。” 匹兹堡。
是否可以找到大小为128的集团的问题是类似的问题。它也可以写为命题公式，并插入到SAT解算器中。从大量的骰子开始，每个骰子有七个点和六种可能的颜色。您可以按规定对点进行着色以使128个骰子可以相互连接吗？换句话说，是否有一种分配颜色的方法可以使派系成为可能？
捕获有关团伙问题的命题公式很长，包含39,000个不同变量。每个值都可以分配两个值（0或1）之一。结果，变量的可能排列或在骰子上排列颜色的方式的数量为2 39,000，这是一个非常非常大的数字。
为了回答凯勒关于第七维的猜想，计算机将必须检查这些组合中的每一个-要么将它们全部排除（意味着不存在大小为128的派系，而凯勒在第七维中是正确的），要么找到一个可行的组合（即凯勒（Keller）是错误的。
Mackey说：“如果您有一台幼稚的计算机检查所有可能的[配置]，则将是这324位案例。” 世界上最快的计算机要用尽所有可能的时间，直到它们耗尽。
但是，这项新工作的作者发现了计算机如何可以得出明确的结论，而不必实际检查所有可能性。效率是关键。
隐藏的效率
Mackey回忆起在他眼中该项目真正成立的那一天。他站在卡内基梅隆大学办公室的黑板前，与Heule和Brakensiek的两位合著者讨论这个问题，当时Heule提出了一种结构化搜索的方法，以便可以合理地完成搜索。时间。
“那天在我办公室里工作的是真正的智力天才，”麦克基说。“就像看着韦恩·格雷茨基，就像在总决赛中看着勒布朗·詹姆斯一样。我现在正想起鸡皮just。”
您可以通过多种方式来增强对特定Keller图的搜索。想象一下，您桌上有很多骰子，而您正试图以满足Keller图规则的方式排列其中的128个。也许您正确地排列了其中的12个模具，但是找不到增加下一个模具的方法。到那时，您可以排除128个骰子的所有配置，其中涉及12个磁贴的不可行的初始配置。
“如果您知道分配给您的前五项内容不匹配，则不必查看其他任何变量，这通常会使搜索范围缩小很多，” 现年60 岁的Shor 说。在麻省理工学院。
效率的另一种形式涉及对称性。当对象是对称的时，我们认为它们在某种意义上是相同的。这种相同性使您可以通过研究对象的一部分来了解整个对象：瞥一下一半的人脸，然后可以重建整个外观。
类似的快捷方式适用于Keller图。再次想象一下，您正在将骰子放在桌子上。也许您从表格的中心开始，然后在左侧建立一个配置。您下了四个骰子，然后撞上了路障。现在，您已经排除了一种初始配置-以及所有基于该配置的配置。但是，您也可以排除该初始配置的镜像，即以相同的方式放置骰子时获得的骰子排列，但要向右扩展。
Hales说：“如果找到一种以智能方式考虑对称性的可满足性问题的方法，那么您将使问题变得更加容易。”
四个合作者以新的方式利用了这种搜索效率-尤其是，他们自动考虑了对称性，以前的工作依靠数学家实际上是手工完成的。
他们最终简化了对大小为128的团体的搜索，因此他们的SAT求解器不必检查2 39,000个配置，而只需要搜索大约10亿个（2 30）。这样一来，搜索就可能变成了千篇一律的杂事。最终，仅经过半个小时的计算，他们便有了答案。
有关：
在我们信任的计算机中？
高尺寸解决球包装
查找复杂信息的通用方法
Heule说：“计算机说不，所以我们知道猜想确实成立。” 无法着色128个骰子，使它们彼此相连，因此凯勒的猜想在第7维上是正确的：覆盖该空间的任何瓷砖排列不可避免地至少包含两个共享一个面的瓷砖。
实际上，计算机提供的不仅仅是一个单词的答案。他们提供了一个长远的证明（大小为200 GB）来证明其结论。
证明不仅仅是读取计算机检查的所有变量配置。这是一个逻辑论点，它确定了所需的集团不可能存在。四名研究人员将Keller证明送入了正式的证明检查器（一种追溯论证逻辑的计算机程序），并确认它可以工作。
Mackey说：“您不仅要审视所有案件，什么也找不到，您要审阅所有案件，并且能够写出证明这件事不存在的证据。” “您能够写出不满意的证明。”
|
