有史以来最大的数学证明：数据多达200TB

[-]
(University of Texas)

德克萨斯大学的三位计算机科学家宣布他们完成了世界上最大的数学证明：完整证明有200TB大小。公开供人检验的部分压缩后也有68GB大。

目前已经有很多数学家使用计算机辅助证明数学问题，但这个200TB大小的证明还是让数学家们吃了一惊。UCSD的数学家Ronald Graham表示，在此之前，世界上最大的数学证明是关于一个离散数学的问题，只有13GB大。

这几位计算机科学家解决的问题有着近一个世纪的历史，是拉姆齐定理中的舒尔平方数定理，也被称为布尔-毕达哥拉斯三元数问题(Boolean Pythagorean triples problem)。该问题在1917年由舒尔提出，问的是：能否将所有正整数分成两个部分，其中所有毕达哥拉斯三元数组(即满足a^2+b^2=c^2的a, b, c三个数)都不处于同一部分？否则，最小的反例是什么？

该类问题常被转化为着色问题来解决。比如如果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种可能方案。德克萨斯大学的Stampede超级计算机的800台处理器共同连续运转了两天两夜才完成了计算。

虽然计算机已经解决了这个布尔-毕达哥拉斯三元数问题，但它并没有告诉我们为什么到了7825时问题就变得无解。这反映了电脑辅助证明中的一个常见的思想挑战：这样“正确”的证明，还算不算是“数学”？如果数学家的工作是通过理论帮助人类更好地理解数学，那通过穷举来解决问题的计算机究竟有什么存在的意义？

或许我们只能希望早日有人给出这个问题的逻辑推理。那个为解决埃尔德什差异问题(Erdős discrepancy problem)的13GB证明提出后仅过了一年，UCLA数学家陶哲轩(相关蛋文：《当今在世的智商最高的十位天才》)就用传统方式成功破解了这一难题，真正震动了全球数学界。

本文译自 Nature & UT Austin，由 zzjeff 编辑发布。