计算机搜索产生“最大”的数学证明

得克萨斯奥斯丁、斯旺西大学和肯塔基大学的三名数学家在超级计算机Stampede的帮助下完成了一个并不优雅的证明，文件大小400TB，这是人类不可能读完的最大数学证明。计算机给出了一个答案，但并没有给出更多的解释，这是计算机辅助证明所带来的哲学上的困惑。研究论文（PDF）发表在预印本网站上。三位数学家解决的是一个布尔可满足性问题，可满足性问题是第一个被证明的NP完全问题。问题是加州圣迭戈数学家Ronald Graham在1980年代提出的，名叫布尔毕达哥拉斯三元数问题：对于自然数集合N={1,2,3,4...}，能否将它们分成两部分，分别以蓝色和红色着色，而满足毕达哥拉斯著名方程 a^2 + b^2 = c^2的数a，b和c不能是同一种颜色。举例来说，对于勾股数3，4，5，如果3和5是蓝色，那么4必须是红色。在计算机的帮助下，研究人员证明，集合N={1，2，...7824} 能满足条件，但到7825时就不可能保证每一个毕达哥拉斯三元数颜色不同。{1，2，...7825} 有10^2300种着色方法，研究人员利用对称性和数论技术设法将计算机需要检查的可能着色方法减少到1万亿以内，然后利用Stampede的800个核心运行了2天。7825这个数有什么特别意义，计算机无法给出解释。