大約十年前，Marijn Heule、Oliver Kullmann 和 Victor Marek 證明了如果你將正整數從 1 到 7825 進行 2 色著色，那麼你必須能夠找到 x、y 和 z，且它們都是同一顏色，滿足 x^2+y^2=z^2——也就是說，一組單色的畢氏三元組。

這解決了 Ron Graham 的一個舊問題。證明是一個龐大的暴力論證。不是純粹的暴力，因為那將是完全不可行的，而是一個使用 SAT 解算器的巧妙暴力計算。 2/

但我相當確定這是以幽默的方式表達，而不是（如Quanta文章中所暗示的）任何形式的批評，因為我現在這樣想，當時也這樣想，這些結果真的很酷。 4/

這個笑話本來是建議人們可以像閱讀更傳統的論證一樣來閱讀這種類型的證明，而在傳統論證中，複雜的案例分析通常被認為有些醜陋。 5/

但當然，這種證明並不是以傳統的方式來閱讀的，並且有其自身的吸引力。就我個人而言，我對使用漂亮的論證將證明簡化為大量計算的想法感到滿意，然後進行計算。 6/

似乎有一些問題，除了這種方法外，實際上無法解決，在這種情況下，我看不出不使用它的理由，我對所得到的理解水平感到滿意。 7/

也就是說，如果有人能找到一個不需要大量案例分析的四色定理的證明（例如），我會慶祝這一點，並將其視為理解上的進步，因為這將解釋為什麼案例分析能夠奏效， 8/

目前我將其視為一種僅僅是事實的情況。同樣地，如果有人能找到一個人類規模的證明來解決畢氏三元組問題，我會感到非常高興。但我非常懷疑這樣的證明是否存在，而這並不困擾我。 9/9