¿Esto es Matemáticas?

Hoy comentamos un reciente resultado sobre matemáticas discretas y teoría de números que pone de nuevo el foco sobre el debate de si las pruebas con ordenador pueden ser consideradas pruebas matemáticas en un sentido estricto.

Un problema que llevaba años sin resolver es el llamado de los triples pitagóricos booleanos. El problema en cuestión, que une dos nombre míticos en la historia de las matemáticas, Pitágoras y George Boole, se plantea de la siguiente forma:

¿Es posible colorear cada entero positivo de rojo o azul de manera que en ningún triple de números enteros a, b y c que satisfaga la ecuación de Pitágoras a² + b² = c² sean todos del mismo color?

Un ejemplo: para el archiconocido triple 3, 4 y 5, si 3 y 5 son azules, entonces 4 no podría ser rojo. Es un problema de interés en Teoría de Ramsey.

En la década de los ochenta, el matemático Ronald Graham ofreció un premio de 100 dólares para la solución del problema, que ahora ha sido otorgado a Marijn Heule, de la University of Texas en Austin. Heule, Oliver Kullmann de Swansea University, UK, y Victor Marek de la University of Kentucky en Lexington demostraron que hay muchas maneras de colorear los enteros hasta 7824, pero cuando pasas a, 7825, es imposible. Son la sorprendentes maravillas de los números y las matemáticas.

Ronald Graham está considerado uno de los mayores expertos mundiales en matemática discreta y es profesor en el California Institute for Telecommunications and Information Technology y es también Irwin y Joan Jacobs Professor en Ciencias de la Computación e Ingeniería en la Universidad de California en San Diego (USCD). El premio puede parecer exiguo, pero la gloria matemática no suele estar hecha de grandes cheques.

Digamos que el artículo en el que se describe la demostración fue publicado en forma de preprint en arXiv el 3 de mayo de este año, y ha sido aceptado para el congreso SAT 2016. Para mas información, digamos que SAT 2016 es el acrónimo del 19th International Conference on Theory and Applications of Satisfiability Testing que se celebrará en el Laboratorio de Ciencia de la Computación de Burdeos del 5 al 8 de julio próximos.

Lo interesante de este resultado es que ha necesitado la ayuda de un supercomputador, el Stampede de la Universidad de Texas. La prueba está condensada en un archivo cuyo tamaño es de 200-terabytes, una auténtica monstruosidad. Y obviamente, Stampede no ha sido capaz de decir por qué ocurre esta rotura de comportamiento en el número 7825. Los matemáticos tendrán que exprimir sus mentes para encontrar la explicación.

La polémica estaba servida con este resultado, y recuerda la famosa prueba de Thomas Hales en 1998 de la conjetura de Kepler. Como en el caso de ahora, Hales tuvo necesidad de usar la computación para examinar la multitud de casos que se le presentaban, y la comunidad matemática tuvo muchos reparos en aceptar la prueba. Finalmente el resultado se publicó en la prestigiosa revista Annals of Mathematicas, de la Universidad de Princeton, con un anexo que contenía el programa de ordenador. Otro caso notable fue la prueba por Kennet Appel y Wolgang Haken en 1976 del Teorema de los cuatro colores, con ayuda también de un ordenador.

Es realmente interesante debatir sobre lo que podemos admitir como prueba, y si el ordenador será capaz de pensar como lo hace un humano cuando trata con un problema matemático. ¡Alan Turing estaría feliz de participar en la discusión!

—

Manuel de León (Fundador del ICMAT, CSIC, Real Academia de Ciencias, Real Academia Canaria de Ciencias, ICSU).