¿Cuál es la forma matemáticamente correcta de apilar naranjas?

Sí, es de un sentido común que alcanza a cualquier verdulero: las manzanas, naranjas o cualquier fruta redonda (o una esfera en general) logran el mejor aprovechamiento del espacio si se apilan como una pirámide. Ya lo había conjeturado el matemático alemán Johannes Kepler en 1611, pero no llegó a demostrarlo.

Tras años de pruebas y estudios, esta semana un grupo de investigadores de la Universidad de Pittsburgh finalmente dio con la demostración matemática de la hipótesis presentada por Kepler.

En 1998, el matemático norteamericano Thomas Hales realizó la primera aproximación a la resolución de esta conjetura, presentando una solución que le permitía comprobar la fiabilidad del modelo. Tras cuatro años de estudio, el jurado de 12 matemáticos encargado de evaluar esta solución confirmó que no había errores en el trabajo de Hales. Sin embargo, declaró que no tenía forma de asegurar que su modelo fuera 100% correcto.

Con este revés en mente, Hales juntó a su equipo de investigadores y se concentró en desarrollar un sistema informático que le permitiera quitar toda duda de su modelo. Así fue como nació el proyecto Flyspeck, un programa creado para verificar paso a paso todas las afirmaciones lógicas de la solución y comprobar que fueran verdaderas (en el sentido lógico del término), ahorrándoles a los matemáticos años de trabajo.

El proyecto Flyspeck, según explicó la revista New Scientist, utilizó dos programas llamados Isabelle y HOL Light, escritos a partir de un kernel mínimo cuyo código fue meticulosamente escrutado para evitar errores, y que permite comprobar la veracidad de cualquier tipo de enunciado lógico.

"Este tipo de tecnología quita a los jurados matemáticos del proceso de verificación" explica Hales, quien vio retrasada la verificación de su hipótesis cuatro años. "Su opinión sobre la corrección de la prueba ya no importa". Hales dice que usará el software para analizar otros enunciados matemáticos.