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.