Há cerca de dez anos, Marijn Heule, Oliver Kullmann e Victor Marek provaram que se você colorir de 2 cores os números inteiros positivos de 1 a 7825, então deve ser possível encontrar x, y e z todos da mesma cor com x²+y²=z² -- ou seja, um triplo pitagórico monocromático.

Isto resolveu um antigo problema de Ron Graham. A prova foi um enorme argumento de força bruta. Não pura força bruta, uma vez que isso teria sido completamente inviável, mas um cálculo de força bruta inteligente usando um solucionador SAT. 2/

Mas estou bastante certo de que foi feito de forma humorística e não (como sugerido no artigo da Quanta) como qualquer tipo de crítica, uma vez que acho agora, e pensava então, que esses tipos de resultados são bastante legais. 4/

A piada teria sido a sugestão de que alguém poderia ler uma prova deste tipo como se fosse um tipo de argumento mais convencional, e análises de casos complicadas em argumentos convencionais são geralmente consideradas um tanto feias. 5/

Mas, claro, uma prova desse tipo não é projetada para ser lida da maneira convencional e tem seu próprio tipo de apelo. Pessoalmente, estou bem com a ideia de usar argumentos bons para reduzir uma prova a um cálculo massivo e, em seguida, fazer o cálculo. 6/

Parece haver alguns problemas que não podem ser realisticamente resolvidos exceto por este tipo de abordagem, caso em que não vejo razão para não a usar, e estou satisfeito com o nível de compreensão resultante. 7/

Dito isto, se alguém encontrasse uma prova do teorema das quatro cores (por exemplo) que não exigisse uma enorme análise de casos, eu celebraria isso e consideraria um avanço na compreensão, uma vez que explicaria por que a análise de casos funcionou, 8/

o que por agora considero como algo que simplesmente acontece. Da mesma forma, se alguém encontrasse um argumento em escala humana para o problema dos tríplos pitagóricos, eu ficaria encantado. Mas duvido muito que tal argumento exista, e isso não me incomoda. 9/9