Hace alrededor de diez años, Marijn Heule, Oliver Kullmann y Victor Marek demostraron que si coloreas en 2 colores los números enteros positivos del 1 al 7825, entonces debes poder encontrar x, y y z todos del mismo color con x^2+y^2=z^2 -- es decir, un trío pitagórico monocromático.

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 ingenioso de fuerza bruta utilizando un solucionador SAT. 2/

Pero estoy bastante seguro de que se pretendía de manera humorística y no (como se sugiere en el artículo de Quanta) como algún tipo de crítica, ya que creo ahora, y pensaba entonces, que este tipo de resultados son bastante geniales. 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 se consideran generalmente 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 realizar el cálculo. 6/

Parece que hay algunos problemas que no se pueden resolver de manera realista excepto mediante este tipo de enfoque, en cuyo caso no veo razón para no usarlo, y estoy satisfecho 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 enorme análisis de casos, lo celebraría y lo consideraría un avance en la comprensión, ya que explicaría por qué el análisis de casos había funcionado, 8/

lo cual, por ahora, considero como algo que simplemente sucede. Del mismo modo, si alguien encontrara un argumento a escala humana para el problema de los tripletas pitagóricas, me encantaría. Pero dudo mucho que exista tal argumento, y eso no me molesta. 9/9