Reseña: Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets

PorJosé A. Alonso

Una de las tareas del razonamiento formalizado consiste en la formalización de textos matemáticos. Un ejemplo es el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets.

El autor del artículo es José Grimm (del INRIA Sophia-Antipolis Méditerranée) y se ha publicado en el Journal of Formalized Reasoning.

El trabajo se enmarca en el proyecto GAIA (Geometry, Algebra, Informatics and Applications), cuyos objetivos son la formalización de las demostraciones del la HDR (Habilitation à diriger des recherches) de A. Quadrat, de las del libro Basic Homological Algebra (de M. Scott Osborne) y la demostración de la corrección de la implementación de estos teoremas como algoritmos en el sistema OreModules.

Dentro del proyecto GAIA, el contenido del artículo es el primer paso y, esencialmente consiste en la formalización en Coq de teoremas del libro Elements of Mathematics: Theory of Sets de N. Bourbaki. La formalización se basa en la realizada por Carlos Simpson y publicada en Set-theoretical mathematics in Coq.

El resumen del artículo es el siguiente

This paper presents a formalization of the first book of the series Elements of Mathematics” by Nicolas Bourbaki, using the Coq proof assistant.

It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki sense, given that the Coq quantifiers are not defined in terms of Hilbert’s epsilon function. The list of axioms and axiom schemes of Bourbaki is compared to the more usual Zermelo-Fraenkel theory, and to those proposed by Carlos Simpson, which form the basis of the Gaia software. Some basic constructions (union, intersection, product, function, equivalence and order relation) are described, as well as some properties; this corresponds to Sections 1 to 6 of Chapter II, and the first two sections of Chapter III. A commented proof of Zermelo’s theorem is also given. The code (including almost all exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.

Interactive Proof: Introduction to Isabelle/HOL

PorJosé A. Alonso

Tobias Nipkow ha publicado un nuevo tutorial de Isabell/HOL: Interactive Proof: Introduction to Isabelle/HOL, que presentará a principio de agosto en la Summer School Marktoberdorf 2011.

El contenido del tutorial es el siguiente:

  • Elementos básicos de Isabelle/HOL: los tipos, términos, fórmulas y teorías.
  • Isabelle/HOL como lenguaje funcional verificable. En esta sección, presenta los tipos básicos (bool, nat y list), cómo pueden definirse funciones y tipos y cómo pueden demostrarse propiedades por inducción y simplificación.
  • Lógica y automatización de las demostraciones. En esta sección, presenta cómo se trabaja con fórmulas y conjuntos, cómo puede automatizarse las demostraciones de sus propiedades y cómo pueden analizarse las demostraciones en pasos elementales.
  • Demostraciones estructuradas con Isar. En esta sección, presenta ejemplos de demostraciones en Isar, patrones de demostraciones, técnicas para mejorar demostraciones y demostraciones por inducción y casos en Isar.

La presentación del tutorial está basada en ejemplos: se concentra en ejemplos que presenta los casos típicos sin explicar el caso general si se puede inferir de los ejemplos.

Las teorías que sirven de ejemplo del tutorial son las siguientes: Overview, Nat, List, Tree, Simp, Induct, Auto_Proof_Demo, Single_Step_Demo, Inductive_Demo, Isar_Demo, Isar_Induct_Demo.

El resto del material utilizado se encuentra en MOD2011.

Reseña – Automated theorem provers: a practical tool for the working mathematician?

PorJosé A. Alonso

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:

  1. 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.
  2. Los demostradores no son lo sufientemente potentes. La potencia de los demostradores está creciendo así como el volumen de matemáticas formalizada.
  3. 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.

Centenario del Principia Mathematica

PorJosé A. Alonso

Con motivo del centenarario de la publicación del primer volumen del Principia Mathematica de Alfred North Whitehead y Bertrand Russell se está publicando distintos artículos conmemorativos.

Hace dos semanas, El País publicó el artículo de José Manuel Sánchez Ron El valor del fracaso digno.

En el artículo se que comenta que aunque el Principia Mathematica de Whithead y Russell no conseguió su fin (reducir la metemática a la lógica) en cambio, por lo riguroso de sus análisis lógicos y la ambiciosa meta que perseguía, se convirtió en una referencia obligada de toda la lógica y la filosofía de la matemática posteriores. En el artículo recuerda la que le escribión de Alice Mary Hilton a Russell: “Estoy segura de que Principia Mathematica no será olvidado mientras exista una civilización que conserve los trabajos de las mentes realmente grandes”. El artículo termina reflexionando sobre los fines y los medios

No hay que esforzarse mucho en argumentar que poner los fines por encima de los medios constituye una perversión que puede destruir una sociedad. Tal vez sí que haya que detenerse más en señalar que el éxito en una empresa no es siempre lo único que se recuerda. También recordamos, debemos recordar, a los que se esforzaron en empresas exigentes. Aunque fracasasen. Como Whitehead y Russell en Principia Mathematica.

Hace unos días se ha publicado un nuevo artículo conmemorativo:
100 Years Since Principia Mathematica, escrito Stephen Wolfram (el autor del sistema de cálculo simbólico Mathematica y del sistema de búsqueda Wolfram Alpha).

El artículo comienza con un comentario sobre un objetivo compartido por los Principia Mathematica y Mathematica: la formalización de las matemáticas. Realiza un recorrido histórico sobre la formalización de la matemática hasta la publicación de los Principia Mathematica. Compara los avances realizados desde los Principia Mathematica en el razonamiento y en el cálculo simbólico:

In the hundred years since Principia Mathematica, there has been slow progress in presenting theorems of mathematics in formal ways. But the idea of mathematical computation has taken off spectacularly — and has transformed the use of mathematics, and many areas of its development.

El artículo termina con una visión del futuro

In the future, however, I suspect that there will be another level of automation. Probably it will take much less than a hundred years, but in time it will become commonplace not just to make computations to order, but to make to order the very systems on which those computations are based—in effect in the blink of an eye inventing and developing something like a whole Principia Mathematica to respond to some particular purpose.