En 1611 Johannes Képler se le ocurrió pensar en cuál sería la mejor manera de apilar una serie de naranjas o manzanas. Su sugerencia fue que una pirámide (para apilar objetos esféricos), sería la mejor solución. Sin embargo, su idea era mera intuición que no podía probar. Pues bien, una computadora finalmente ha demostrado esta vieja conjetura.
Un matemático ha anunciado el final de una búsqueda épica (y diría yo, frenética) para formalmente probar la llamada conjetura de Képler. “Me he quitado un gran peso de encima”, dijo Thomas Hales, de la Universidad de Pittsburgh, Pennsilvania, quien fue el líder de este trabajo. “De pronto sentí como si fuese 10 años más joven”, aseguró al saber que la prueba era correcta.
Hales primero presentó una prueba de que la intuición de Képler era correcta en 1998. Y aunque hay un infinito número de maneras de colocar un infinito número de esferas, la mayoría son solamente variaciones de un par de miles de temas. Hales decidió entonces utilizar la técnica top-down, que se usa frecuentemente en la resolución de programas de software, es decir, romper en pequeñas partes las miles de posibles formas de acomodar las esferas y representar matemáticamente estas posibilidades infinitas. Una vez hecho esto, puso a la computadora, con un programa especial creado por él, a checar todas las posibilidades.
La prueba tiene unas 300 páginas que le tomó a 12 revisores cuatro años para verificar que no hubiese errores. Fue entonces cuando se publicó en el “Annals of Mathematics” el resumen de este trabajo, en el 2005. Los revisores indicaron que ellos podían decir que el “99% era cierto”, por lo que consideraron la prueba como correcta.
En el 2003, Hales inició un proyecto al que bautizó con el nombre de Flyspeck, que buscaría demostrar formalmente esta verificación. Su equipo de trabajo usó dos programas de computadora, llamados Isabelle y HOL Light, los cuales están diseñados para trabajar con proposiciones lógicas y que busca exhaustivamente por posibles errores. Esto le llevó a entender que la computadora podría verificar una serie de proposiciones lógicas para confirmar que fuesen verdaderas.
El equipo de trabajo anunció que finalmente habían traducido toda la prueba matemática de Hales en la forma computarizada y verificado que era correcta.
“Esta tecnología podría abreviar a los revisores en matemáticas para los procesos de verificación”, dice Hales. “Su opinión sobre la corrección de la prueba ya no importa realmente”, dijo.
“Ha sido un enorme esfuerzo”, dijo Alan Bundy, de la Universidad de Edinburgo, en el Reino Unido, quien no está involucrado en el trabajo. Añadió que espera que el éxito del proyecto Flyspeck inspire a otros matemáticos a usar estos ayudantes de pruebas en matemáticas.
Por lo que respecta a Hales, dice que está listo para seguir adelante. Tiene una caja llena de ideas que ha dejado sin trabajar mientras analizaba su demostración formal.
“¡Esperemos que el siguiente proyecto no lleve 20 años!”, expresó.
Referencias: New Scientist