Heule, Kullmann y Marek son tres matemáticos que han resuelto con uno de los superordenadores de la Universidad de Texas uno de los problemas que desde hace décadas ha estado eludiendo a los expertos de los números: una cuestión combinatoria sobre las llamadas ternas pitagóricas booleanas (más conocidas por ser del tipo a²+b²=c²).
Lo más interesante es que para resolverlo utilizaron la potencia de un superordenador: un clúster de 800 procesadores, trabajando ininterrumpidamente durante 48 horas recopiló la solución en un gigantesco archivo de 200 terabytes. Lo hizo comprobando una por una las combinaciones de ternas coloreadas de rojo y azul de todas las ternas necesarias para ver si había alguna en las que no tuvieran todos el mismo color.
Este método de «demostración asistida por ordenador» se utilizó por primera vez en 1976 en la demostración del teorema de los cuatro colores. Con los primitivos ordenadores de la época en aquella época requirió según sus autores «1.200 horas de cálculos, 50 páginas de texto y diagramas, 85 páginas con otros 2.500 diagramas adicionales y 400 páginas de microfichas además de miles de verificaciones a mano». Podemos suponer que fueron unos pocos MB o algún GB, si acaso.
Aunque estas cosas siempre son un poco relativas, comparativamente los 200 TB de esta demostración serían 200.000 veces más información (como mínimo), verificada 25 veces más rápido: un poderío unas 5 millones de veces superior el de los equipos actuales.
En Arxiv se puede leer el trabajo original: Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer donde también se indica cómo acceder a los 200 TB del fichero de la demostración (por si alguien tiene interés) que comprimido se queda en unos mejores 68 GB, algo mucho más manejable.
Por cierto que como suele suceder en estos casos primero hubo que hacer todos los cálculos y luego comprobarlos. Algo que, «filosóficamente» supone un problema para algunos matemáticos puristas, que consideran que demostraciones como estas no son realmente «demostraciones» – porque no se puede asegurar que tanto el cálculo como la comprobación estén libres de errores. De hecho muchos miran con cara de asco casos como este, como si fueran demostraciones bastardas y repelentes.
(Vía Futurism.)
