最长数学证明破解世界难题：看完需100亿年

　　上世纪80年代，美国数学家罗伯特-格拉汉姆悬赏100美元，请数学爱好者帮助他解决一个数学难题，这道数学难题困扰了格拉汉姆很长时间。三十多年来，一直未能有人拿出破解方案前来领赏。近日，一个由美英两国三位数学家组成的研究团队宣称他们应该得到这笔奖金。

　　但是，数学同行们发现，这个研究团队所得出的结论同样也很难验证，因为他们是利用超级计算机证明出来的，证明的过程非常复杂，堪称世界最长的数学证明，阅读全部的证明文件需要花费100亿年。

　　他们利用一台超级计算机解决了这个数学难题，他们表示：“我们对这个数学难题有着共同的兴趣。我们的结果还需要一个正式的证明。”

　　这个所谓的世界难题被称为“布尔毕氏三元数问题”，是毕达哥拉斯定理(勾股定理)方面的问题，即关于直角三角形各条边的长度之间的关系问题。

　　在平面直角三角形中，两个直角边边长的平方加起来等于斜边长的平方，即著名的数学公式：a^2 b^2=c^2。

　　格拉汉姆提出一个疑问，如果每一条边长都是一个正整数，并给这个正整数分配一种颜色，或蓝色或红色，满足上述公式的正整数是否都是同一颜色呢?格拉汉姆认为答案是否定的。

　　简单地说，满足上述公式的任何三个正整数，只可能是两个是一种颜色，另一个是另外一种颜色 ，他们不可能是相同颜色的。

　　布尔毕氏三元数问题

　　该类问题常被转化为着色问题来解决，比如，如果3和5被用红色标记，那么4必需用蓝色标记。

　　研究者发现，从1到7824的所有正整数都能被用这种方式归类。

　　在这7824个方格中，没有任何满足a^2 b^2=c^2的三个数同为蓝色或同为红色。(白色数字不属于毕达哥拉斯三元数。)

　　在Marijn Heule、Oliver Kullmann和Victor Marek三人发表在arXiv上的这篇论文里，他们把该问题拆分称了两个SAT可满足性问题，然后发现该问题达到 {1,…,7825} 时无解，最后展示了自己给7824个方格上色的方法。

　　有关拉姆齐定理的设想往往涉及着巨量的数据，这个问题更不例外。在有这么多数字的情况下，给方格上色的可能方案达到了10^2300那么多，但研究者借助了对称分析等技法，让电脑只需要检查10^12种可能方案。

　　数学家发现，数字在1到7824之间时，这个问题可以得到证明和解决，但是，当数字超过7824时，问题就无解了。

　　三位数学家利用“分块攻克”的混合可满足性测试方法，证明了布尔毕氏三元数问题。

　　他们的研究成果发表于著名的预印本网站arXiv之上，并在波尔多召开的一次会议上演示了证明结果。

　　据了解，证明文件的字符总和相当于美国国会图书馆所有数码资料的总和，大小约200TB。即使利用德州先进运算中心的Stampede超级计算机对这些数据进行压缩，也需要花两天时间。

　　虽然从技术上讲，三位数学家的确利用超级计算机对这个问题进行了证明和解决，但是，问题依然存在。

　　其中一个问题是，这个证明是否真的是一个完善的证明?它其实还没有回答为什么会在7825这个数字上出现无解现象。

　　尽管如此，现已80高龄的格拉汉姆早已准备好奖金，毕竟超级计算机已经给出了一个答案。