Asi před deseti lety Marijn Heule, Oliver Kullmann a Victor Marek dokázali, že pokud 2-barevně obarvíte kladná celá čísla od 1 do 7825, pak musíte být schopni najít x, y a z všechny stejné barvy s x^2+y^2=z^2 -- to je monochromatická pythagorejská trojice. 1/

Tím se vyřešil starý problém Rona Grahama. Důkazem byl masivní argument hrubou silou. Ne čistou hrubou silou, protože ta by byla naprosto neproveditelná, ale chytrým výpočtem hrubou silou pomocí SAT řešiče. 2/

Ale jsem si docela jistý, že to bylo míněno vtipně a ne (jak je naznačeno v článku Quanta) jako nějaký druh kritiky, protože si myslím teď, a myslel jsem si tehdy, že tento druh výsledků je docela v pohodě. 4/

Vtip by spočíval v tom, že by se důkaz tohoto typu mohl číst, jako by šlo o konvenčnější druh argumentu, a komplikované případové analýzy v konvenčních argumentech jsou obecně považovány za poněkud ošklivé. 5/

Důkaz tohoto druhu ale samozřejmě není určen k tomu, aby byl čten konvenčním způsobem, a má svůj vlastní druh přitažlivosti. Osobně mi nevadí myšlenka použití pěkných argumentů k redukci důkazu na masivní výpočet a pak tento výpočet provést. 6/

Zdá se, že existují určité problémy, které nelze reálně vyřešit jinak než tímto druhem přístupu, v takovém případě nevidím důvod, proč jej nepoužít, a jsem spokojen s výslednou úrovní porozumění. 7/

To znamená, že pokud by někdo našel důkaz čtyřbarevné věty (například), který by nevyžadoval rozsáhlou případovou analýzu, oslavoval bych to a považoval bych to za pokrok v porozumění, protože by to vysvětlovalo, proč případová analýza vyšla, 8/

což prozatím považuji za něco, co se prostě stane. Podobně, pokud by někdo našel argument v lidském měřítku pro problém pythagorejských trojic, pak bych byl potěšen. Ale velmi pochybuji, že takový argument existuje, a to mě netrápí. 9/9