困扰数学家90年的猜想,被计算机搜索30分钟解决了
数学家会代码,就连困扰人类 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 猜想,去年陶哲轩已经“几乎”解决了这个问题,现在可能只差一步之遥了。
参考链接:
https://www.quantamagazine.org/computer-search-settles-90-year-old-math-problem-20200819/
https://www.cs.cmu.edu/~mheule/Keller/
https://mathworld.wolfram.com/KellerGraph.html
论文地址:
https://arxiv.org/abs/1910.03740
源代码:
https://github.com/marijnheule/Keller-encode
— 完 —