数学家会代码，就连困扰人类90年的数学猜想也挡不住。
来自斯坦福、CMU等高校的4名数学家，直接将一个数学难题转化成了对10亿个结果进行
“暴力搜索”。
△ 论文作者之一CMU助理教授Marijn Heule
他们把这串代码输入40台电脑组成的计算集群，30分钟后，计算机给出了一个200GB大小
的证明结果：
凯勒猜想在不超过7维的空间上都是正确的。
现在，任何人都可以去GitHub上克隆这串代码，验证这一数学定理。
比较反转的是，这段获得计算机学术会议IJCAR（国际自动推理联合会议）最佳论文奖的
程序，上线GitHub半年，只揽获了一颗星。
那么，这4位数学家要证明的“凯勒猜想”到底是什么？为何非要用计算机来证明？计算
机证明的结果可靠吗？
下面让我们一一道来。
什么是凯勒猜想
假如用一批完全相同的正方形瓷砖铺满地面，中间不留空隙。显然，瓷砖之间会共用一
条边，如下图蓝线所示：
在3维空间中，如果要用立方体占满空间，是不是也和2维空间类似呢？
想象一下，如果像下图那样在空间中随便放入几个立方体，由此展开填满整个空间，那
么唯一的办法就是让接上的立方体共用蓝色的面。
2维、3维皆如此，更高维度的空间会怎样？
1930年，德国数学家凯勒猜测，如果用n维立方体填满无限空间，则立方体之间必然会出
现“面对面”，对于任意维度都成立。
这便是凯勒猜想。
但数学猜想不能仅靠直觉，必须有严格的证明。90年来，数学家一直不懈努力。
1940年，数学家Perron证明了凯勒猜想在1到6维空间是正确的。
1992年，另外两位数学家Lagarias和Shor证明，凯勒猜想在10维空间上是错误的。
（注：这位Shor就是那个提出用量子计算机求解质因数分解的Shor算法的数学家。）
非常不幸，凯勒猜想竟然是错的！然而问题并没有到此结束。
还有3个维度没有解决呢！在7维、8维、9维三个维度空间中，凯勒猜想是否成立？
只要解决这三个维度，缠绕数学家几十年的问题就彻底搞定了。
数学论证表明，如果凯勒猜想在n维空间上是错的，那么它在比n更高的维度上也一定是
错的。
2002年，数学家Mackey已证明，凯勒猜想在8维空间不成立，因此在9维空间也不成立。
至此，7维空间成为唯一的难题。
△ 证明8维空间凯勒猜想错误的CMU教授Mackey
证明方法的改进
可能你已经发现，从上世纪90年代以来，凯勒猜想的证明速度大大加快，数学家只用了
10年时间就把问题缩小到三个维度。
这主要得益于两位数学家的贡献。
当年，Perron求解1到6维时，没有特殊的捷径。而到1990年，凯勒猜想的证明方法发生
了巨大的变化。
数学家Corrádi和Szabó提出了一种新的思路，把原来无限空间的问题变成有限的、离
散的问题，也让计算机解决凯勒猜想成为可能。
他们巧妙地把凯勒猜想变成了图论问题，就是构造所谓的凯勒图（Keller Graph），而
图论正是计算机所擅长的。
在这种方法的指导下，Lagarias和Shor两人很快在2年后就证明了10维空间的情况：凯勒
猜想不成立。又过了10年，Mackey证明，凯勒猜想在8维空间不成立。
那么，凯勒图究竟是什么，它为什么能够加速凯勒猜想的证明？
构造“凯勒图”
首先，我们从最简单的2维情况说起。
现在，我们有一种牌，牌上画着两个有颜色的点。两个点是有顺序的，不能调换。比如
，1黑2白≠1白2黑。
两个点总共可以涂4种颜色，颜色分成2对：红色对绿色、白色对黑色。
数学家已经证明，分配给点的颜色相当于正方形在空间中的坐标。两张牌的颜色是否配
对表示两个正方形的相对位置。
点的颜色与正方形的具体关系是这样的：
1、两对点完全相同，表示两个正方形完全重叠
2、两对点颜色都不同，且颜色都不配对，表示两个正方形有部分重叠
3、一对点颜色相同，另一对点颜色配对，表示两个正方形共用一个边
4、一对点颜色不同，另一对点颜色配对，表示两个正方形的边相互接触但不重合
2个点的凯勒图，要用2对颜色去填充牌面，总共有16种情况。
然后我们把这16张牌摆在桌上，只有符合前面条件4的两张牌，才用线将二者连起来。这
样就构成了一张“凯勒图”。
包含16张牌的凯勒图就描绘了正方形填补平面的所有可能。
如果2维空间中凯勒猜想不成立，那么我们肯定能找到4个正方形，它们之间没有共用的
边，但是能够无缝隙填在一起。然后在屏幕上无限复制这4个正方形，就能填满整个屏幕
。
实际上并不可能。如果按此操作，只会得到有着无数孔隙（下图紫色部分）的填充方式
。
对应到凯勒图中，就是找在图中找到4张牌，它们两两之间都有连线。（在数学里，这叫
做完全图。）
显然，在2维问题的凯勒图中，我们找不到这样的4张牌。（可以自己去上面的凯勒图中
找找看。）
这样，我们把就把n维立方体以及位移s与牌的点数n、颜色对数s联系起来。
作为更一般的规则，如果要证明n维凯勒猜想是错的，就要在对应的凯勒图中找到2n张牌
，且这些牌两两相连。
正因为你找不到4个张牌组成的完全图，所以2维空间的凯勒猜想是对的。
为了在3维空间中证明凯勒猜想，可以使用216张牌，每张牌上3个点，并可以使用3对颜
色（这一点相对灵活）。然后，我们需要寻找23=8张牌 ，它们两两之间都有连线，但还
是找不到。
到了8维空间中，我们总算可以找到符合条件的256张牌，所以8维空间的凯勒猜想是错的
。
△8维空间中的一个反例（一个凯勒图的完全子图）
接下来的事情就是在7维空间对应的凯勒图上寻找完全子图。然而这个问题却从8维问题
解决后被搁置了17年。
根据前面的说明，求解8维空间和10维空间的凯勒猜想，要寻找28=256和210=1024张牌的
子图，而7维空间只要寻找27=128张牌的子图。
后者的难度似乎更小，7维空间的问题应该更简单啊！其实不然。
因为，从某种意义上说，8维和10维可以“分解”为容易计算的较低维度，但7维不行。
证明了10维情况的Lagarias说：“7维不好，因为它是质数，这意味着你无法将其分解为
低维。因此别无选择，只能处理这些图的全部组合。”
对于人脑来说，寻找大小为128的子图是一项艰巨的任务，但这恰恰是计算机擅长回答的
问题。
计算机帮忙
说干就干，此前证明8维问题的CMU教授Mackey拉上了斯坦福的数学在读博士Brakensiek
和专长计算机辅助证明的助理教授Heule。
回忆起立项的那天，Mackey说，Brakensiek是真正的天才，看着他就像看着NBA总决赛里
的詹姆斯。Brakensiek本人确实很厉害，他曾是2013/14两届国际信息学奥赛金牌得主。
△ 论文第一作者Brakensiek
言归正传。为了方便计算机求解，他们换了个方向来思考：
先设定牌上有7个点、6种可能的颜色，按照前面的“条件4”对这些牌上色，看看能不能
找到128种不同的填色方法。如果找不到，那么凯勒猜想成立。
用计算机辅助证明数学问题，还需要把它变成一系列逻辑运算，也就是处理01之间的与
或非关系。
若要求解7维，则总共包含39000个不同布尔变量（0或1），有239000种可能性，这是一
个非常非常大的数字，有11741位数。
△2的39000次方（来自Wolfram Alpha运算结果）
一台普通电脑只能处理324位数种可能，离解决问题还远得很。就算交给超级计算机也不
够。
但是，这几位数学家想到了排除法，只要得到结论，而不必实际检查所有可能性。效率
才是王道！
比如，用计算机规则给128张牌上色，当你涂到第12张牌的时候，发现找不到符合条件的
下一张牌了。那么所有包含这12张牌的排列都可以排除。
提升效率的另一种方式是利用对称性。如果已经验证了某种排列不可能，那与之对称的
所有情况都可以排除。
通过这两种方法，他们把搜索空间缩小到10亿（230）。这样一来，用计算机搜索变成了
可能。
最终，他们仅计算了半个小时，便有了答案。
计算机没有找到符合条件的128张牌，所以7维空间的凯勒猜想确实成立。
实际上，计算机提供的不仅仅是一个答案，证明的内容多达200GB。4位论文作者将证明
送入计算机的证明检查器，确认了它的可靠性。
解决了凯勒猜想后，Heule的下一个目标是用计算机证明数学里“最简单的不可能问题”
——3n+1猜想，去年陶哲轩已经“几乎”解决了这个问题，现在可能只差一步之遥了。
--
FROM 113.102.160.*