转载

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

　　得克萨斯奥斯丁、斯旺西大学和肯塔基大学的三名数学家在超级计算机 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 这个数有什么特别意义，计算机无法给出解释。

正文到此结束