În urmă cu aproximativ zece ani, Marijn Heule, Oliver Kullmann și Victor Marek au demonstrat că dacă colorezi 2 numerele întregi pozitive de la 1 la 7825, atunci trebuie să fii capabil să găsești x, y și z toate de aceeași culoare cu x^2+y^2=z^2 -- adică o triplă pitagoreică monocromatică. 1/

Acest lucru a rezolvat o veche problemă a lui Ron Graham. Dovada a fost un argument masiv de forță brută. Nu forță brută pură, deoarece ar fi fost complet imposibilă, ci un calcul inteligent de forță brută folosind un rezolvator SAT. 2/

Dar sunt destul de sigur că a fost intenționat cu umor și nu (așa cum se sugerează în articolul Quanta) ca orice fel de critică, deoarece cred acum, și am crezut atunci, că acest tip de rezultate sunt destul de interesante. 4/

Gluma ar fi fost sugestia că cineva ar putea citi o demonstrație de acest tip ca și cum ar fi un tip de argument mai convențional, iar analizele complicate de caz în argumentele convenționale sunt în general considerate oarecum urâte. 5/

Dar, desigur, o demonstrație de acest fel nu este concepută pentru a fi citită în mod convențional și are propriul său tip de atracție. Personal, sunt de acord cu ideea de a folosi argumente frumoase pentru a reduce o demonstrație la un calcul masiv și apoi de a face calculul. 6/

Se pare că există unele probleme care nu pot fi rezolvate în mod realist decât prin acest tip de abordare, caz în care nu văd niciun motiv să nu o folosesc și sunt mulțumit de nivelul de înțelegere rezultat. 7/

Acestea fiind spuse, dacă cineva ar găsi o demonstrație a teoremei în patru culori (de exemplu) care nu ar necesita o analiză de caz uriașă, aș sărbători asta și aș privi-o ca pe un progres în înțelegere, deoarece ar explica de ce analiza de caz a funcționat, 8/

ceea ce deocamdată consider ceva care se întâmplă să fie cazul. De asemenea, dacă cineva ar găsi un argument la scară umană pentru problema triplelor lui Pitagora, atunci aș fi încântat. Dar mă îndoiesc foarte mult că există un astfel de argument și asta nu mă deranjează. 9/9