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 formal que pudiera verificarse con software de comprobación de pruebas automatizado, como HOL Light e Isabelle.
Este proyecto se denominó Flyspeck, una ampliación del acrónimo FPK, que significa «Formal Proof of Kepler» (Prueba formal de Kepler). Al inicio de este proyecto, en 2007, Hales estimó que producir una prueba formal completa llevaría alrededor de 20 años de trabajo, sin embargo, la finalización del proyecto se anunció el 10 de agosto de 2014. En efecto, Hales y 21 colaboradores publicaron un artículo titulado «A formal proof of the Kepler conjecture» (Una prueba formal de la conjetura de Kepler) en arXiv, en el que afirmaban haber demostrado la conjetura, y en 2017, la prueba formal fue aceptada por la revista Forum of Mathematics.
El demostrador automático de teoremas Isabelle es un demostrador de teoremas de lógica de orden superior HOL, acrónimo de Higher-Order Logic, que es un lenguaje fuertemente tipado con estructuras de datos, funciones recursivas (incluyendo valores funcionales) y expresiones lógicas con cuantificadores. A principios de la década de 1980, Larry Paulson desarrolló Cambridge LCF basándose en trabajos anteriores de Robin Milner. Lawrence Charles Paulson es un informático estadounidense, profesor de Lógica Computacional en el Laboratorio de Informática de la Universidad de Cambridge.HOL es esencialmente el LCF de Cambridge con una lógica diferente (lógica de orden superior). Isabelle estaba escrito en Standard ML y Scala. Standard ML (SML) es un lenguaje de programación funcional modular, de alto nivel y uso general con comprobación de tipos en tiempo de compilación e inferencia de tipos. Scala, por su parte, es un lenguaje de programación de alto nivel, fuertemente tipado y de propósito general, que admite tanto la programación orientada a objetos como la programación funcional.
Isabelle está disponible dentro de un marco de sistema flexible que permite extensiones lógicamente seguras, que comprenden tanto teorías como implementaciones para la generación de código, la documentación y el soporte específico para una variedad de métodos formales. Se puede considerar como un entorno de desarrollo integrado (IDE) para métodos formales.
En los últimos años, se ha recopilado un número considerable de teorías y extensiones del sistema en el Archivo Isabelle de Pruebas Formales (Isabelle AFP).
Como curiosidad, digamos que Isabelle fue bautizada así por Larry Paulson en honor a la hija de Gérard Pierre Huet, informático, lingüista y matemático francés, director de investigación sénior en el INRIA (Institut national de recherche en informatique et en automatique) y conocido principalmente por sus importantes y fundamentales contribuciones a la teoría de tipos, la teoría de los lenguajes de programación y la teoría de la computación.
_____________
Manuel de León (CSIC, Fundador del ICMAT, Real Academia de Ciencias, Real Academia Canaria de Ciencias, Real Academia Galega de Ciencias, Presidente del ICM2006 Madrid y miembro del Comité Ejecutivo de IMU (2007-2024) y del Comité Ejecutivo del ISC (2014-2018).