Około dziesięć lat temu Marijn Heule, Oliver Kullmann i Victor Marek udowodnili, że jeśli pokolorujesz liczby całkowite dodatnie od 1 do 7825 na dwa kolory, to musisz być w stanie znaleźć x, y i z w tym samym kolorze, gdzie x^2+y^2=z^2 -- to znaczy, monochromatyczną potrójną Pythagorejską.

To rozwiązało stary problem Rona Grahama. Dowód był ogromnym argumentem opartym na metodzie prób i błędów. Nie czystą metodą prób i błędów, ponieważ to byłoby całkowicie niewykonalne, ale sprytnym obliczeniem opartym na metodzie prób i błędów z użyciem solvera SAT. 2/

Ale jestem prawie pewien, że to miało być humorystyczne, a nie (jak zasugerowano w artykule Quanta) jako jakakolwiek krytyka, ponieważ myślę teraz, a myślałem wtedy, że tego rodzaju wyniki są całkiem fajne. 4/

Żart polegałby na sugestii, że można by przeczytać dowód tego typu tak, jakby był bardziej konwencjonalnym rodzajem argumentu, a skomplikowane analizy przypadków w konwencjonalnych argumentach są zazwyczaj uważane za dość brzydkie. 5/

Ale oczywiście dowód tego rodzaju nie jest zaprojektowany do czytania w konwencjonalny sposób i ma swój własny rodzaj uroku. Osobiście, nie mam nic przeciwko pomysłowi używania ładnych argumentów, aby zredukować dowód do masowej obliczeń, a następnie wykonać obliczenia. 6/

Wydaje się, że istnieją pewne problemy, które nie mogą być realistycznie rozwiązane inaczej niż w ten sposób, w takim przypadku nie widzę powodu, aby z tego nie skorzystać, i jestem zadowolony z uzyskanego poziomu zrozumienia. 7/

To powiedziawszy, jeśli ktoś znalazłby dowód twierdzenia o czterech kolorach (na przykład), który nie wymagałby ogromnej analizy przypadków, świętowałbym to i uznałbym za postęp w zrozumieniu, ponieważ wyjaśniłoby to, dlaczego analiza przypadków zadziałała, 8/

które na razie uważam za coś, co po prostu jest. Podobnie, jeśli ktoś znalazłby argument w skali ludzkiej dla problemu potrójnych Pythagorejskich, byłbym zachwycony. Ale bardzo wątpię, że taki argument istnieje, i to mnie nie martwi. 9/9