![]()
La conjetura de Kepler e Isabelle
En la entrada previa, hablamos de la conjetura de Kepler y como fue resuelta por Thomas Hales, con la ayuda de los ordenadores. Vamos ahora a comentar cuál fue en concreto esa ayuda. Como decíamos, en enero de 2003, Hales anunció el inicio de un proyecto colaborativo para producir una prueba formal completa de la conjetura de Kepler, a fin de eliminar cualquier incertidumbre que pudiera quedar sobre la misma. Lo que tenía en la cabeza era crear una prueba…