Matemáticos dirigidos por Thomas Hales de la Universidad de Pittsburgh han presentado una prueba formal de la conjetura de Kepler, un problema de la geometría sin solución en más de 300 años.
La conjetura de Kepler es un famoso problema de la geometría discreta que aborda la manera más eficiente de amontonar esferas en un espacio dado.
La respuesta, no tan difícil de suponer, ha sido sumamente difícil de comprobar. El famoso matemático y astrónomo Johannes Kepler dio la respuesta hace 300 años, pero no pudo demostrarla, informa Cambridge.org.
En 1998, el profesor Hales y su estudiante Sam Ferguson anunciaron una primera prueba, pero la solución era muy larga y complicada, por lo que un equipo de árbitros dedicó años antes de descartarla.
«La prueba fue publicada en 2005 y no se encontraron fallos irreparables, pero la insatisfactoria situación era que la prueba parecía ir más allá de lo que podía revisar a fondo la comunidad de matemáticas», dijo Henry Cohn, editor de Forum of Mathematics, Pi –que ha publicado el nuevo trabajo– e investigador de Microsoft Research New England en Cambridge, Massachusetts.
«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 a extraordinario detalles utilizando una estricta lógica formal, lo que un programa informático revisó con perfecto rigor. Este artículo es el resultado del trabajo», indicó Cohn.
El 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, indicó Cambridge University Press, la más antigua editorial universitaria.
Fuente: Europa Press