Propuesta de una base de datos informática de todo el conocimiento matemático
El manifiesto QED fue una propuesta para una base de datos basada en computadora de todo el conocimiento matemático , estrictamente formalizada y con todas las pruebas verificadas automáticamente . ( QED significa quod erat demonstrandum en latín , es decir, "que debía demostrarse").
Descripción general
La idea del proyecto surgió en 1993, principalmente bajo el impulso de Robert Boyer . Los objetivos del proyecto, llamado provisionalmente proyecto QED o proyecto QED , se describieron en el manifiesto QED, un documento publicado por primera vez en 1994, con aportes de varios investigadores. [1] Se evitó deliberadamente la autoría explícita. Se creó una lista de correo dedicada y se llevaron a cabo dos conferencias científicas sobre QED, la primera en 1994 en los Laboratorios Nacionales de Argonne y la segunda en 1995 en Varsovia organizada por el grupo Mizar . [2]
El proyecto parece haberse disuelto en 1996, sin haber producido nunca más que debates y planes. En un artículo de 2007, Freek Wiedijk identifica dos razones para el fracaso del proyecto. [3] En orden de importancia:
- Son muy pocas las personas que trabajan en la formalización de las matemáticas. No existe ninguna aplicación convincente para las matemáticas totalmente mecanizadas.
- Las matemáticas formalizadas aún no se parecen a las matemáticas tradicionales reales. Esto se debe en parte a la complejidad de la notación matemática y en parte a las limitaciones de los probadores de teoremas y los asistentes de demostración existentes ; el artículo concluye que los principales contendientes, Mizar , HOL y Coq , tienen serias deficiencias en sus capacidades para expresar las matemáticas.
No obstante, se proponen regularmente proyectos de estilo QED. La Biblioteca Matemática Mizar formaliza una gran parte de las matemáticas de grado y fue considerada la biblioteca más grande de este tipo en 2007. [4] Entre los proyectos similares se incluyen la base de datos de pruebas Metamath y la biblioteca mathlib escrita en Lean . [5]
En 2014 se organizó el taller Veinte años del Manifiesto QED [6] como parte del Verano de Lógica de Viena .
Véase también
Referencias
- ^ El Manifiesto QED en Deducción Automatizada - CADE 12 , Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, págs. 238-251, 1994. Versión HTML
- ^ Informe del taller QED II
- ^ Freek Wiedijk, El manifiesto QED revisitado, 2007
- ^ Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel y JB Wells, Informatización gradual/formalización de textos matemáticos en Mizar
- ^ Biblioteca Mathlib https://leanprover-community.github.io/mathlib-overview.html
- ^ Veinte años del taller del Manifiesto QED
Lectura adicional
- H. Barendregt y F. Wiedijk, El desafío de las matemáticas informáticas , Transactions A of the Royal Society 363 no. 1835, 2351–2375, 2005
- "Número especial sobre la demostración formal". Avisos de la American Mathematical Society . Diciembre de 2008.(problema de acceso abierto)
- Richard A. De Millo , Richard J. Lipton , Alan J. Perlis , Procesos sociales y pruebas de teoremas y programas , Communications of the ACM , Volumen 22, Número 5 (mayo de 1979), Páginas: 271 - 280
- John Harrison, Matemáticas formalizadas , Informe técnico 36, Centro de Ciencias de la Computación de Turku (TUCS)
- Ittay Weiss, El Manifiesto QED después de dos décadas Versión 2.0 , Journal of Software vol. 11, no. 8, pp. 803-815, 2016.
Enlaces externos
- Freek Wiedijk, Formalización de 100 teoremas Una página que registra el progreso en la formalización de 100 teoremas comunes.
- Freek Wiedijk, Los diecisiete demostradores del mundo, una prueba de la irracionalidad de la raíz cuadrada de dos en diecisiete asistentes de prueba diferentes.
- Matemáticas Formalizadas es una revista en la que se presentan las pruebas de Mizar.
- El Archivo de Pruebas Formales es un repositorio similar (con referato) de pruebas en Isabelle/HOL.
- [1] Un depósito de pruebas en Coq.
- UniMath "La biblioteca Coq tiene como objetivo formalizar un cuerpo sustancial de matemáticas utilizando el punto de vista univalente "
