Razonamiento formalizado: Del sueño a la realidad de las pruebas
Jean-Paul Delahaye ha publicado en Interstices un artículo panorámico sobre razonamiento asistido por ordenador titulado Du rêve à la réalité des preuves. Una versión anterior de este trabajo se publicó en la revista Pour la Science.
El artículo comienza con una pequeña historia del razonamiento formalizado. Comienza con el sueño de Leibniz en el siglo XVII de reducir el razonamiento al cálculo. El sueño fue parcialmente realizado por los Principia Mathematica (1910-13) de Alfred Whitehead y Bertrand Russell en los que se intenta reducir las matemáticas a la lógica. En esta obra se muestra cómo las matemáticas pueden ser formalizables en teoría, pero no en la realidad (ya que la formalización que proponen es demasiado compleja para realizarla prácticamente). A este trabajo le han sucedido otras formalizaciones, como la de Bourbaki en los años 30, basada en la teoría de conjuntos pero con parecidos inconvenientes.
Sin embargo, la informática y un siglo de trabajo de los lógicos han hecho realidad el sueño y logrado formalizaciones prácticas y reales de las matemáticas. El primer trabajo de formalización de las matemáticas fue el proyecto Automath desarrollado por Nicolaas de Bruijn a partir de 1966. Su trabajo fue seguido por otros proyectos como Mizar, HOL, Isabelle y Coq. La idea de estos asistentes de prueba es poner a disposición del usuario un sistema interactivo y un formalismo que le permita elaborar una versión formal de conomiento matemático.
Una forma de mostrar el éxito obtenido con los asitentes de prueba en la formalización de las matemáticas es comprobando las formalizaciones de los 100 principales teoremas de la lista de Nathan Kahn. Actualmente se ha formalizado el 87% de la lista entre los que destacan las demostraciones de
- la irracionalidad de la raiz cuadradada de 2,
- la infinitud de los números primos,
- la imposibilidad de la trisección de un ángulo,
- el teorema de Lagrange de los cuatro cuadro
- la fórnula de Leibniz para π: π/4= 1 – 1/3 + 1/5 – 1/7 + 1/9 – …
- la divergencia de la serie armónica,
- el teorema fundamental del álgebra
- el teorema fundamental del cálculo integral,
- la transcendencia de e,
- el primer teorema de incompletitud de Gödel,
- el teorema de los números primos y
- el teorema de los cuatro colores.
Algunos de los 13 teoremas de la listas pendientes de formalizar son
Aparte de las anteriores formalizaciones de los anteriores teoremas, la utilidad de los asistentes de prueba se aprecia en los teoremas enormes como el de Thomas Hales que resuelve la conjetura de Kepler o el de clasificación de los grupos simples.
Otro campo de aplicación de los asistentes de prueba se encuentra en la verificación de programas y sistemas informáticos.
A pesar de los éxitos obtenidos se plantean varios problemas como son:
- la confianza en la corrección en los propios asistentes de prueba. Se consigue aumentarla reduciendo el núcleo del sistema a pocas líneas que sen simples y legibles, comprobando los núcleos con numerosos ejemplos y demostrando la correción de los núcleos con otros asistentes de prueba.
- la dificultad del trabajo de formalizar (que se traduce en más de un día de trabajo para formalizar una página de texto matemático),
- la escasa utilización de los asistentes en la investigación matemática, aunque especialistas como Henk Barendregt y Freek Wiedijk vaticinan que en el próximo decenio producirán un cambio en los hábitos de investigación matemática.