Certificación computacional del conocimiento matemático

PorJosé A. Alonso

Esta entrada está dedicada a los antecentes de la certificación computacional del conocimiento matemático en estilo declarativo.

Por lo que respecta a la verificación declarativa, sus raices se encuentran en el trabajo realizado en el proyecto Mizar. El proyecto Mizar comenzó en el 1973 como un intento de reconstruir la matemática en un entorno computacionalmente certificable. Los teoremas demostrados dentro del proyecto Mizar se encuentran fundamentalmente en la Mizar Mathematical Library y en la revista Formalized Mathematics que se publica desde el año 1990. El sistema Mizar no es automático sino que es sólo un verificador. Por contra, los sistemas de demostración no disponían de modos de demostración declararativa hasta que M. Wenzel creó Isar (Intelligible semi-automated reasoning). Isar está construido sobre el sistema Isabelle. Isabelle es un asistente de prueba genérico desarrollado por L. Paulson (en la Universidad de Cambridge) y T. Nipkow (en la Universidad Politécnica de Munich). Las teorías formalizadas en Isabelle/Isar se encuentran fundamentalmente en la biblioteca de Isabelle2009-1, en la revista The Archive of Formal Proofs y en la IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment).

Por lo que respecta a la certificación computacional del conocimiento
matemático los antecedentes pueden situarse en el 1993 con la publicación del manifiesto del proyecto QED impulsado por Bob Boyer y la revisión del proyecto QED en 2007 por F. Wiedijk. Actualmente se han demostrado muchos teoremas matemáticos importantes, como puede comprobarse en Formalizing 100 Theorems, en la NASA Langley PVS Libraries y en The Coq Users’ Contributions. Entre los teoremas formalmente certificados podemos citar el teorema de de la distribución de los números primos, el teorema de los cuatro colores y el teorema de la curva de Jordan. Nuestro grupo posee experiencia en la certificación de teoremas matemáticos habiendo certificado en ACL2 y PVS, entre otros, el lema de Newman, el teorema de Knuth-Bendix, el teorema de corrección del algoritmo de Buchberger, el teorema de Bezem de completitud de la resolución proposicional y el teorema de completitud de la resolución SLD.

Reto de formalización: El proyecto Wiles-Fermat

PorJosé A. Alonso

Una de las líneas de desarrollo de la Lógica Computacional es abordar formalizaciones de resultados matemáticos complejos. El intento de formalización produce como efectos laterales la formalización del conocimiento implícito en el resultado (el mathware) y el desarrollo de nuevos procedimientos de decisión.

Uno de los grandes retos actuales es la formalización de la demostración de Andrew Wiles del último teorema de Fermat. Una descripción detallada del reto se encuentra en el artículo Computer verification of Wiles’ proof of Fermat’s Last Theorem de Wim H. Hesselink. En el artículo se traza la hoja de ruta de la formalización describiendo la estructura de la demostración de Wiles. Una de las principales dificultades radica en comentando la necesidad de disponer de sistemas de razonamiento que incorporen cálculo simbólico. Hesselink estima que se tardarán unos 50 años en conseguirse la formalización del teorema de Wiles.