Cerca de dez anos atrás, Marijn Heule, Oliver Kullmann e Victor Marek provaram que se você 2 colore os inteiros positivos de 1 a 7825, então você deve ser capaz de encontrar x, y e z todos da mesma cor com x ^ 2 + y ^ 2 = z ^ 2 - isto é, um triplo pitagórico monocromático. 1/

Isso resolveu um velho problema de Ron Graham. A prova foi um argumento maciço de força bruta. Não força bruta pura, já que isso teria sido totalmente inviável, mas um cálculo inteligente de força bruta usando um solucionador SAT. 2/

Mas tenho certeza de que foi feito com humor e não (como sugerido no artigo Quanta) como qualquer tipo de crítica, já que acho agora, e pensava então, que esses tipos de resultados são muito legais. 4/

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

Mas é claro que 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 bons argumentos 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 resolvidos de forma realista, exceto por esse tipo de abordagem, caso em que não vejo razão para não usá-la e estou feliz com o nível de compreensão resultante. 7/

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

o que, por enquanto, considero algo que por acaso é o caso. Da mesma forma, se alguém encontrasse um argumento em escala humana para o problema dos triplos pitagóricos, eu ficaria encantado. Mas duvido muito que tal argumento exista, e isso não me incomoda. 9/9