数学|困扰数学家90年的猜想，被计算机搜索30分钟解决了
晓查 发自 凹非寺
量子位 报道 | 公众号 QbitAI
数学家会代码 ， 谁也挡不住！就连困扰人类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位论文作者将证明送入计算机的证明检查器 ， 确认了它的可靠性 。
【数学|困扰数学家90年的猜想，被计算机搜索30分钟解决了】解决了凯勒猜想后 ， Heule的下一个目标是用计算机证明数学里“最简单的不可能问题”——3n+1猜想 ， 去年陶哲轩已经“几乎”解决了这个问题 ， 现在可能只差一步之遥了 。
推荐阅读
![[玩懂手机]三星多款Galaxy A系列新机发布：价格适中](http://ttbs.guangsuss.com/image/cfbf354f7d258c9914fed797e2fc6456)
- 数学|【2021年阿贝尔奖获得者】LászlóLovász 传记
- 许晨阳|北大数学天才许晨阳，获我国100万美元奖金，却留三条理由去美国
- 炎症性肠病|柳叶刀子刊：关注炎症性肠病患者的抑郁焦虑困扰｜研究速递
- 数学|百年纽结问题迎来突破
- 伯恩哈德·黎曼|羞怯的数学家黎曼，有着太阳一样辉耀的心
- 植物神经系统|一个困扰患者7年的疾病，药没少吃，病却没好！
- 数学|徐一鸿：数学在基础物理中的有效性——威格纳之后三十年
- 脊柱|快帮爸妈看看，别让这个常见疾病困扰他们的晚年生活
- 春季过敏性鼻炎|春季过敏性鼻炎来犯，做好这些可缓解你的鼻炎困扰
- 周毓麟|巨星陨落！两院院士、著名数学家周毓麟逝世