La conjetura de Kepler fue formulada por el físico, matemático y astrónomo alemán Johannes Kepler en 1611. Esta conjetura afirma que si apilamos esferas iguales, la densidad máxima se alcanza con una apilamiento piramidal de caras centradas. Esta densidad es aproximadamente del 74%.
En 1998 Thomas Hales anunció que había demostrado la conjetura de Kepler. Fue publicada en Annals of Mathematics. La comprobación de Hales es una demostración por casos en la que se prueban agrupamientos mediante complejos cálculos de computadora. Hales formuló una ecuación de 150 variables que recogía cinco mil posibles agrupamientos de esferas iguales.
Los doce científicos seleccionados por Annals para realizar la revisión por pares comentaron que estaban al "99% seguros" de la exactitud de la prueba de Hales, pero que era imposible revisar los tres gigabytes de códigos. Sin embargo, el método utilizado por Hales en la demostración no es exhaustivo, por lo que no está dilucidado el problema. Por tanto, la conjetura de Kepler está más cerca de convertirse en un teorema.
El autor de la solución se dedicó a crear el proyecto Flyspeck, consistente en un programa que verifica paso a paso todas las afirmaciones lógicas de la solución matemática, verificándola en lugar de los propios matemáticos. El 9 de agosto de 2014, el equipo de Hales anunció que el programa que crearon logró verificar la solución de la Conjetura de Kepler propuesta por Hales, y que no encontró errores.
“Esta tecnología excluye a los árbitros matemáticos del proceso de verificación. Su opinión sobre la corrección de las pruebas ya no importa más”, afirma Hales, citado por la revista ‘New Scientist‘. La prueba del problema, verificada por una computadora, puede abrir una nueva era en las matemáticas donde las máquinas harán el “trabajo pesado” liberando a los científicos para que se puedan dedicar al “pensamiento más profundo”.
En junio de 2017, la demostración formal de la Conjetura de Kepler fue aceptada en la revista Forum of Mathematics.[1]​