难点是把搜索范围缩小到十亿，并且写出验证代码吧。算法有了机器就是钱的事，这个规模租一下云计算很便宜。
【 在 PlayerUnkwn 的大作中提到: 】
:
: 数学家会代码，就连困扰人类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猜想，去年陶哲轩已经“几乎”解决了这个问题，现在可能只差一步之遥了。
:
: --
:
发自「今日水木 on LYA-AL00」
--
FROM 123.118.31.*