For rundt ti år siden beviste Marijn Heule, Oliver Kullmann og Victor Marek at hvis du 2-farger de positive heltall fra 1 til 7825, så må du være i stand til å finne x, y og z alle av samme farge med x^2+y^2=z^2 -- det vil si en monokromatisk pytagoreisk trippel. 1/

Dette løste et gammelt problem med Ron Graham. Beviset var et massivt rå kraftargument. Ikke ren brute force, siden det ville vært helt ugjennomførbart, men en smart brute-force-beregning ved hjelp av en SAT-løser. 2/

Men jeg er ganske sikker på at det var ment humoristisk og ikke (som foreslått i Quanta-artikkelen) som noen form for kritikk, siden jeg synes nå, og tenkte da, at denne typen resultater er ganske kule. 4/

Vitsen ville ha vært antydningen om at man kunne lese et bevis av denne typen som om det var en mer konvensjonell type argumentasjon, og kompliserte kasusanalyser i konvensjonelle argumenter blir generelt sett på som noe stygge. 5/

Men selvfølgelig er et bevis av denne typen ikke designet for å bli lest på den konvensjonelle måten, og har sin egen form for appell. Personlig har jeg det bra med ideen om å bruke fine argumenter for å redusere et bevis til en massiv beregning og deretter gjøre beregningen. 6/

Det ser ut til å være noen problemer som ikke realistisk kan løses annet enn ved denne typen tilnærming, i så fall ser jeg ingen grunn til ikke å bruke det, og jeg er fornøyd med det resulterende forståelsesnivået. 7/

Når det er sagt, hvis noen skulle finne et bevis for firefargeteoremet (for eksempel) som ikke krevde en stor kasusanalyse, ville jeg feire det og betrakte det som et fremskritt i forståelsen, siden det ville forklare hvorfor kasusanalysen hadde fungert, 8/

som jeg foreløpig ser på som noe som tilfeldigvis er tilfelle. På samme måte, hvis noen skulle finne et argument i menneskelig skala for Pythagoras trippelproblem, ville jeg bli glad. Men jeg tviler sterkt på at et slikt argument eksisterer, og det plager meg ikke. 9/9