Hace unos diez años, Marijn Heule, Oliver Kullmann y Victor Marek demostraron que si se colorean los enteros positivos de 1 a 7825, entonces se debe poder encontrar x, y y z todos del mismo color con x ^ 2 + y ^ 2 = z ^ 2, es decir, un triple pitagórico monocromático. 1/

Esto resolvió un viejo problema de Ron Graham. La prueba fue un argumento masivo de fuerza bruta. No pura fuerza bruta, ya que eso habría sido completamente inviable, sino un cálculo inteligente de fuerza bruta utilizando un solucionador SAT. 2/

Pero estoy bastante seguro de que fue con humor y no (como se sugiere en el artículo de Quanta) como ningún tipo de crítica, ya que creo ahora, y pensé entonces, que este tipo de resultados son bastante buenos. 4/

La broma habría sido la sugerencia de que uno podría leer una prueba de este tipo como si fuera un tipo de argumento más convencional, y los análisis de casos complicados en argumentos convencionales generalmente se consideran algo feos. 5/

Pero, por supuesto, una prueba de este tipo no está diseñada para ser leída de la manera convencional y tiene su propio tipo de atractivo. Personalmente, estoy de acuerdo con la idea de usar buenos argumentos para reducir una prueba a un cálculo masivo y luego hacer el cálculo. 6/

Parece que hay algunos problemas que no se pueden resolver de manera realista excepto con este tipo de enfoque, en cuyo caso no veo ninguna razón para no usarlo, y estoy contento con el nivel de comprensión resultante. 7/

Dicho esto, si alguien encontrara una prueba del teorema de los cuatro colores (por ejemplo) que no requiriera un gran análisis de casos, lo celebraría y lo consideraría como un avance en la comprensión, ya que explicaría por qué el análisis de casos ha funcionado, 8/

lo que por ahora considero como algo que simplemente es el caso. Del mismo modo, si alguien encontrara un argumento a escala humana para el problema de los triples pitagóricos, entonces estaría encantado. Pero dudo mucho que exista tal argumento, y eso no me molesta. 9/9