La conjetura de Kepler es un famoso problema que aborda la manera más eficiente de amontonar esferas en un espacio dado; la respuesta ha sido sumamente difícil de comprobar. El famoso matemático y astrónomo alemán Johannes Kepler dio el resultado hace 300 años, pero no pudo demostrarlo.
El profesor de la Universidad de Pittsburgh, Thomas Hales, y su estudiante Sam Ferguson, presentaron una primera prueba en 1998; pero la solución era muy larga y complicada, por lo que un equipo de árbitros dedicó años antes de descartarla.
Ahora, para abordar esta situación y establecer certidumbre, Hales recurrió a las computadoras y utilizó técnicas de verificación formal. El y sus colaboradores escribieron toda una prueba utilizando una estricta lógica formal, lo que un programa informático revisó con perfecto rigor.
Cambridge University Press, la más antigua editorial universitaria, indicó por su parte que el reciente artículo no sólo resuelve un problema matemático de siglos, sino que también es un gran impulso para la verificación informática de pruebas matemáticas complejas.
Crónica Digital /PL
