Por Gizmodo
¿Cuál es la manera más eficiente de apilar naranjas o manzanas? Suena banal, pero esa pregunta llevaba 400 años sin respuesta científica. En 1611, el astrónomo y matemático alemán Johannes Kepler planteó, casi por pura intuición, que la mejor manera de apilar objetos esféricos era formando una pirámide, pero ni Kepler ni los que le han seguido han podido probar nunca esa conjetura.
Aunque probablemente todos los fruteros del mundo dirían que esto es evidente, para demostrar científicamente el problema hacen falta buenas dosis de cálculo. En 1998, Thomas Hales, de la Universidad de Pittsburgh, en Pennsylvania, desarrolló una serie de ecuaciones que probaban la validez de la conjetura de Kepler.
El estudio tenía 300 páginas, y las 12 personas encargadas de su verificación tardaron cuatro años en comprobar todos los cálculos. Incluso así, el estudio de Hales solo probaba la teoría de la pirámide en un 99%. En 2003, Hales puso en marcha el proyecto Flyspeck, un software que pudiera probar sin atisbo de duda la teoría de Kepler.
Hales desarrolló dos programas llamados Isabelle y HOL Light. Ambos están especializados en aplicar relaciones de lógica en busca de errores en una teoría matemática. Este domingo, Isabelle y HOL Light han completado su análisis. La conjetura de Kepler es 100% correcta. La noticia no solo es positiva para Hales, quien asegura haberse quitado 10 años de encima. Su éxito abre la puerta al desarrollo de aplicaciones para solucionar cuestiones matemáticas que siguen sin resolver debido a cálculos demasiado tediosos. [vía New Scientist]