Formal Proof
T. Hales Formal Proof. Notices of the AMS, Vol. 55, N. 11 (2008) p.1370-1380.
Este trabajo es el primer artículo del número de Diciembre de 2008 de las Notices of the AMS dedicado a las demostraciones formales.
El artículo comienza comentando los errores de programación (estima que se cometen 1.5 errores por línea cuando escribe código).
En la sección 1 comenta la certidumbre en matemáticas y sus problemas: supuestos implícitos (p.e. en la geometría griega) y demostraciones muy complejas (p.e. la de Almgren que ocupa 1.728 páginas). Así como el papel de los ordenadores en su certificación.
En la sección 2 trata de las demostraciones formales frente a las tradicionales. Comenta la dificultad de pasar de las segundas a la primera y recoge una tabla con algunas de las principales demostraciones formalizadas.
La sección 3 la dedica a comentar un sistema de razonamiento: el HOL Light. La elección debe de ser porque es en el que él trabaja. Contiene una detallada descripción de la lógica del sistema.
La sección 4 trata de sistemas de demostración automática. Comenta que no se han cumplido las profecías de la IA (1965)
- a digital computer will discover and prove an important new mathematical theorem.
Sin embrago se han obtenido algunos éxitos como la demostración de la conjetura de Robbins, las demostraciones geométricas con el método de Wu y los procedimientos de decisión en algunas teorías.
La sección 5 trata del descubrimiento automático, desde el AM de Lenat hasta Graffiti.pc.
La sección 6 la dedica al proyecto Flyspec cuyo objetivo es la demostración formal de la conjetura de Kepler. Este proyecto es la razón por la que el autor se interesó por las demostraciones formalizadas. Cuenta la historia de la prueba de la conjetura y del proyecto.
La sección 7 la dedica al proyecto QED. Inscribe el proyecto Flyspec dentro de los objetivos del manifiesto QED. Termina proponiendo el reto de la secuenciación del genoma matemático:
- To undertake the formalization of jus 100, 000 pages of core mathematics would be one of the most ambitious collaborative projects eve undertaken in pure mathematics, the sequencing of a mathematical genome. One might imagine a massive wiki collaboration that settles the text o the most significant theorems in contemporary mathematics from Poincaré to Sato-Tate.
El artículo es de lectura agradable y resulta muy estimulante.
José A. Alonso 11 Diciembre 2008
