Circa dieci anni fa, Marijn Heule, Oliver Kullmann e Victor Marek hanno dimostrato che se colori i numeri interi positivi da 1 a 7825 con 2 colori, allora devi essere in grado di trovare x, y e z tutti dello stesso colore con x^2+y^2=z^2 -- cioè, un triplo pitagorico monocromatico. 1/

Questo ha risolto un vecchio problema di Ron Graham. La dimostrazione era un enorme argomento di forza bruta. Non pura forza bruta, poiché sarebbe stata completamente inattuabile, ma un'astuta computazione di forza bruta utilizzando un risolutore SAT. 2/

Ma sono abbastanza sicuro che fosse inteso in modo umoristico e non (come suggerito nell'articolo di Quanta) come una sorta di critica, poiché penso ora, e pensavo allora, che questi tipi di risultati siano davvero interessanti. 4/

La battuta sarebbe stata il suggerimento che si potrebbe leggere una prova di questo tipo come se fosse un tipo di argomento più convenzionale, e le analisi di casi complicati negli argomenti convenzionali sono generalmente considerate piuttosto brutte. 5/

Ma certo, una prova di questo tipo non è progettata per essere letta nel modo convenzionale e ha il suo fascino. Personalmente, mi va bene l'idea di usare argomenti validi per ridurre una prova a un'enorme computazione e poi eseguire la computazione. 6/

Sembra che ci siano alcuni problemi che non possono essere risolti realisticamente se non con questo tipo di approccio, nel qual caso non vedo motivo per non utilizzarlo, e sono soddisfatto del livello di comprensione risultante. 7/

Detto ciò, se qualcuno dovesse trovare una prova del teorema dei quattro colori (per esempio) che non richiedesse un'enorme analisi dei casi, lo celebrerei e lo considererei un progresso nella comprensione, poiché spiegherebbe perché l'analisi dei casi avesse funzionato, 8/

che per ora considero come qualcosa che semplicemente è così. Allo stesso modo, se qualcuno dovesse trovare un argomento di scala umana per il problema dei tripli pitagorici, sarei deliziato. Ma dubito molto che un tale argomento esista, e questo non mi disturba. 9/9