Vor etwa zehn Jahren bewiesen Marijn Heule, Oliver Kullmann und Victor Marek, dass wenn man die positiven ganzen Zahlen von 1 bis 7825 mit 2 Farben färbt, man x, y und z finden muss, die alle die gleiche Farbe haben, mit x²+y²=z² -- das heißt, ein monochromatisches pythagoreisches Tripel.

Dies löste ein altes Problem von Ron Graham. Der Beweis war ein massives Brute-Force-Argument. Nicht reines Brute Force, da das völlig unpraktisch gewesen wäre, sondern eine clevere Brute-Force-Berechnung mit einem SAT-Löser. 2/

Aber ich bin mir ziemlich sicher, dass es humorvoll gemeint war und nicht (wie im Quanta-Artikel vorgeschlagen) als irgendeine Art von Kritik, da ich jetzt denke und damals dachte, dass diese Art von Ergebnissen ziemlich cool ist. 4/

Der Witz wäre der Vorschlag gewesen, dass man einen Beweis dieser Art lesen könnte, als wäre er eine konventionellere Art von Argument, und komplizierte Fallanalysen in konventionellen Argumenten werden im Allgemeinen als etwas hässlich angesehen. 5/

Aber natürlich ist ein Beweis dieser Art nicht dafür gedacht, auf die herkömmliche Weise gelesen zu werden, und hat seine eigene Art von Anziehungskraft. Persönlich finde ich die Idee, schöne Argumente zu verwenden, um einen Beweis auf eine massive Berechnung zu reduzieren und dann die Berechnung durchzuführen, in Ordnung. 6/

Es scheint einige Probleme zu geben, die realistisch gesehen nur mit dieser Art von Ansatz gelöst werden können, in diesem Fall sehe ich keinen Grund, ihn nicht zu verwenden, und ich bin mit dem daraus resultierenden Verständnis zufrieden. 7/

Das gesagt, wenn jemand einen Beweis für den Vierfarben-Satz (zum Beispiel) finden würde, der keine umfangreiche Fallanalyse erfordert, würde ich das feiern und als Fortschritt im Verständnis betrachten, da es erklären würde, warum die Fallanalyse funktioniert hat, 8/

was ich derzeit als etwas betrachte, das einfach der Fall ist. Ebenso wäre ich erfreut, wenn jemand ein menschliches Argument für das Problem der pythagoreischen Tripel finden würde. Aber ich bezweifle sehr, dass ein solches Argument existiert, und das stört mich nicht. 9/9