El artículo Automated theorem provers: a practical tool for the working mathematician? de Alan Bundy se ha publicado el 16 de julio en Annals of Mathematics and Artificial Intelligence.
En el artículo se analiza la utilización de los sistemas de demostración asistida por ordenador (SDAO) en la investigación matemática. Se parte del hecho de que los SDAO se usa por los matemáticos menos que otros sistemas informáticos (como LaTeX o los sistemas de cálculo simbólico). Pero, su interés ha aumentado en la última década, como puede observarse en el número de Diciembre de 2008 de las Notices of the AMS dedicado a las demostraciones formales. El autor conjetura que este interés seguirá creciendo e influirá en la metodología matemática.
Entre las causas de este creciente interés destaca la aparición de teoremas con grandes demostraciones (como el teorema de los cuatros colores, la conjetura de Kepler y la clasificación de los grupos finitos) en cuya demostración se ha usado ordenadores. Se ha críticado el uso de los ordenadores en la demostración, por la posibilidad de que los programas tuviesen errores. Para asegurar su corrección se ha formalizado (en el caso del teorema de los cuatro colores) o se está formalizando (en los otros dos) su demostración mediante SDAO.
Otros razones para el aumento del interés en los SDAO se encuentra en nuevas aplicaciones como síntesis automática de teoremas, automatización de la refactorización de demostraciones, búsqueda de teoremas, automatización de la revisión de artículos y automatización de la corrección de exámenes.
Por otra parte, entre las razones para la resistencia del uso de los SDAO y sus posibles soluciones, apunta las siguientes:
- Las demostraciones formalizadas son demasiadas detalladas y largas. Se puede mejorar presentando las demostraciones jarárquicamente de forma que se pueda elegir el nivel de detalle y los pasos esenciales de las pruebas.
- Los demostradores no son lo sufientemente potentes. La potencia de los demostradores está creciendo así como el volumen de matemáticas formalizada.
- Los demostradores son difíciles de usar. Los desarrolladores de los sistemas están mejorando los interfaces. Una mejora significativa es el uso de demostraciones declarativas (como en Isar).
Personalmente, pienso que la principal barrera está en disponer de una buena base de conocimiento formalizado utilizable en distintos SDAO y de herramientas de búsqueda semántica en dicha base de conocimiento. Además, entre las posibles aplicaciones de los SDAO creo que también será importante su uso como ayudantes en la docencia como describe Benjamin C. Pierce en Using a Proof Assistant to Teach Programming Language Foundations.