La manera más eficiente de apilar objetos redondos, como naranjas o manzanas, es en pirámide, así lo planteó el matemático alemán Johannes Kepler en 1611. Sin embargo, ¿cómo comprobar esa conjetura si resulta de pura intuición? Aunque te paresca difícil de creer, ese problema matemático llevaba 400 años sin solución hasta hoy.
Thomas Hales, de la Universidad de Pittsburgh, presentó un estudio de 300 páginas en 1998 para comprobar, a través del cálculo, la supuesta efectividad del planteamiento de Kepler. El trabajo, que tardó unos cuatro años de elaboración, solo comprobó el 99% de la teoría de la pirámide.
Lejos de rendirse, Hales inició en 2003 el proyecto Flyspeck, un software que probaría la mencionada teoría. Luego desarrolló dos programas más llamados Isabelle y HOL Light, ambos especializados en la aplicación de relaciones de lógica para comprobar la efectividad de una teoría matemática. Recién el pasado domingo, Isabelle y HOL Light han completado su análisis, señalando que la conjetura de Kepler es 100% correcta.
Este primer éxito iniciará el futuro desarrollo de aplicaciones para solucionar y comprobar cuestiones matemáticas que siguen en el terreno de la duda.