Antes de la llegada de la computadora a nuestras vidas, los matemáticos «arrastraban el lápiz» continuamente, es decir, las demostraciones se buscaban dando argumentos, deduciendo, induciendo en algunos casos, etcétera. Hoy en día la computadora la usan los matemáticos para ayudarse a probar teoremas o conjeturas no resueltas antes. Una de ellas, por ejemplo, es la conjetura de los cuatro colores, que dice que se necesitan solamente cuatro colores, en un mapa de dos dimensiones, de manera que dos regiones adyacentes (o países) no tengan el mismo color.

Hoy en día se acepta que las computadoras pueden ser una buena herramienta para las pruebas matemáticas, sin embargo, en el caso que ahora nos ocupa, se requirieron unos 200 terabytes para lograr la demostración. El problema a resolver se llama el de los triples pitagóricos, el cual es (o fue), un problema abierto en la teoría de Ramsey, el cual dice así: ¿Puede un conjunto de números naturales, 1, 2, 3, … ser dividido en dos partes de tal manera que ninguna de las partes contenga un triple pitagórico? (es decir, que contenga tres números que formen los lados de un triángulo rectángulo de forma que $latex a^2 + b^2 = c^2$)

El problema de los dos conjuntos es el más básico y es fácil dictar el enunciado por probar pero mucho más difícil resolverlo o demostrarlo. Por ejemplo, podemos poner el caso de 3, 4 y 5, los cuales cumplen con la fórmula descrita, pero 5 es otro triple: 5, 12 y 13. Por lo que no podemos poner en el mismo conjunto que el 5. Pero 12 y 13 son dos triples, 12, 35, 37 y 13, 84, 85. Puede verse que empieza a ser un problema ver cómo localizar estos números y cada vez se vuelve más difícil. La pregunta es pues ¿puede demostrarse la conjetura enumerando quizás todas las posibilidades?

Hay un premio que ha esperado 20 años para darse y ahora sabemos que la respuesta a la pregunta es no, pero la prueba es notable por sí misma. En principio, lo que hay que hacer es simplemente hallar un contraejemplo, pero por lo que hemos dicho, se vuelve cada vez más difícil añadir más y más números. El mejor resultado hasta ahora ha sido el conjunto {1,2,3,,, 7624} que puede ser particionado, por lo que para encontrar un contraejemplo hay que ir más allá del 7624 y 7625.

El artículo donde se describe la prueba, se checó que n=7624 tiene una partición que puede satisfacer la condición por un par de segundos: simplemente se exhibe la partición y se checa que no hay triples en cada parte. Por otra parte, el probar que con n=7625 no tiene tal partición involucra ver cada una de las posibles particiones,

Para resolver el problema, se usó Stampede, la súper computadora del centro avanzado de cómputo de Texas, que tiene 270 terabytes de RAM, 14 petabytes de almacenamiento en disco y 522080 núcleos. Con ello, los investigadores hallaron la manera de explorar todas las posibilidades, pero se estimó que el cálculo llevaría 35 mil horas de CPU, dato que obligó a los investigadores a buscar otra posibilidad. Se decidió usar un clúster con 800 núcleos del mismo centro de cómputo, el cual halló la solución en aproximadamente dos días.

Se uso un «SAT Solver», que es un programa que solamente da como resultado «sí» o «no», es decir, si «puede o no satisfacer la fórmula». Cuando se tuvo el resultado, se empezó a trabajar en la «prueba final», la cual requirió 200 terabytes de datos, que comprimidos ocupan unos 68 gigabytes. Claramente estos datos son para usarse con un programa, no tienen ningún sentido para los seres humanos.

Así pues, lo que sabemos es que el problema de los triples pitagóricos con k=2 se puede resolver para n<7825 pero es imposible para n más grande. La pregunta es si podría haber una prueba matemática más corta. Si es así, debería poderse encontrar una estructura lógica que encapsula la aparente complejidad de la enumeración para las particiones que no pueden satiusfacer la condición. No se sabe si esto es posible, por lo que la prueba al menos es una mera enumeración de todos los posibles resultados que pueden o no satisfacer la condición del problema.

Referencias:

Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer, Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek
i-programmer