大约十年前，Marijn Heule、Oliver Kullmann 和 Victor Marek 证明了，如果你对从 1 到 7825 的正整数进行 2 色着色，那么你必须能够找到 x、y 和 z，它们都是同一种颜色，并且满足 x^2+y^2=z^2——也就是说，一个单色的毕达哥拉斯三元组。 1/

这解决了 Ron Graham 的一个老问题。证明是一个庞大的暴力论证。不是纯粹的暴力，因为那将是完全不可行的，而是使用 SAT 求解器的巧妙暴力计算。 2/

但我很确定这句话是出于幽默，而不是（正如Quanta文章中所暗示的）任何形式的批评，因为我现在认为，也曾认为，这种结果非常酷。 4/

这个笑话本来是建议人们可以像阅读更传统的论证那样阅读这种类型的证明，而在传统论证中，复杂的案例分析通常被认为有些丑陋。 5/

但当然，这种类型的证明并不是为了以传统方式阅读而设计的，它有自己独特的吸引力。就我个人而言，我对使用漂亮的论证将证明简化为大量计算，然后进行计算的想法感到满意。 6/

似乎有一些问题，除了通过这种方法外，实际上无法解决，在这种情况下，我看不出不使用它的理由，我对所得到的理解水平感到满意。 7/

也就是说，如果有人能找到一个不需要大量案例分析的四色定理的证明（例如），我会为此庆祝，并将其视为理解上的进步，因为这将解释为什么案例分析能够奏效， 8/

就目前而言，我认为这只是一个事实。同样，如果有人能找到一个适合人类规模的毕达哥拉斯三元组问题的论证，我会很高兴。但我非常怀疑这样的论证是否存在，这并不困扰我。 9/9