Noin kymmenen vuotta sitten Marijn Heule, Oliver Kullmann ja Victor Marek osoittivat, että jos 2-värjäät positiiviset kokonaisluvut 1:stä 7825:een, sinun on pystyttävä löytämään x, y ja z kaikki samaa väriä x^2+y^2=z^2:lla -- eli monokromaattinen Pythagoraan kolmois. 1/

Tämä ratkaisi Ron Grahamin vanhan ongelman. Todisteena oli massiivinen raa'an voiman argumentti. Ei puhdasta raakaa voimaa, koska se olisi ollut täysin mahdotonta, vaan älykäs raa'an voiman laskenta SAT-ratkaisijalla. 2/

Mutta olen melko varma, että se oli tarkoitettu humoristisesti eikä (kuten Quantan artikkelissa ehdotetaan) minkäänlaiseksi kritiikiksi, koska olen sitä mieltä, että nyt ja silloin ajattelin, että tällaiset tulokset ovat aika siistejä. 4/

Vitsi olisi ollut ehdotus, että tämäntyyppistä todistusta voitaisiin lukea ikään kuin se olisi tavanomaisempi argumentti, ja monimutkaisia tapausanalyysejä tavanomaisissa argumenteissa pidetään yleensä jokseenkin rumana. 5/

Mutta tietenkään tällaista todistusta ei ole suunniteltu luettavaksi tavanomaisella tavalla, ja sillä on omanlaisensa vetovoimansa. Henkilökohtaisesti olen tyytyväinen ajatukseen käyttää mukavia argumentteja todistuksen pelkistämiseksi massiiviseksi laskelmaksi ja sitten tehdä laskelma. 6/

Näyttää siltä, että on joitain ongelmia, joita ei realistisesti voida ratkaista muuten kuin tällaisella lähestymistavalla, jolloin en näe mitään syytä olla käyttämättä sitä, ja olen tyytyväinen tuloksena olevaan ymmärryksen tasoon. 7/

Jos joku kuitenkin löytäisi (esimerkiksi) nelivärilauseesta todisteen, joka ei vaatisi valtavaa tapausanalyysiä, juhlisin sitä ja pitäisin sitä edistysaskeleena ymmärryksessä, koska se selittäisi, miksi tapausanalyysi oli toiminut, 8/

mitä toistaiseksi pidän asiana, joka vain sattuu olemaan totta. Samoin, jos joku löytäisi ihmisen mittakaavan argumentin Pythagoraan kolmoisongelmalle, olisin iloinen. Mutta epäilen vahvasti, että sellaista argumenttia on olemassa, eikä se häiritse minua. 9/9