Il manifesto QED è stato il progetto internazionale di una banca dati informatizzata di tutte le conoscenze matematiche, formalizzate rigorosamente e con tutte le dimostrazioni verificate mediante software automatici (in latino QED è l'acronimo di quod erat demonstrandum).
Storia
[modifica | modifica wikitesto]L'idea del progetto nacque nel 1993 sotto l'impulso di Robert Boyer. L'anno successivo, un gruppo di ricercatori sottoscrisse un documento programmatico la cui paternità rimase deliberatamente sconosciuta.[1] Fu creata una mailing list le cui attività culminarono in due conferenze, tenutesi nel '94 presso gli Argonne National Laboratories e nel '95 a Varsavia, organizzate dal gruppo che gestiva il progetto Mizar.[2]
Il progetto sembra essersi dissolto nel 1996, non avendo mai prodotto altro che discussioni e progetti. In un documento del 2007, Freek Wiedijk identificò due ragioni per il fallimento del progetto, che in ordine di importanza erano[3]:
- il numero limitatissimo di persone che lavorano alla formalizzazione della matematica; l'inesistenza di un'applicazione capace di automatizzare in modo convincente le dimostrazioni matematiche;
- la formalizzazione matematica mediante la teoria degli insiemi è un'attività molto diversa dalla matematica tradizionale. Ciò è dovuto in parte alla complessità della notazione matematica, e in parte ai limiti dei dimostratori di teoremi e degli assistenti di dimostrazione esistenti; il documento rileva che i principali competitor, quali Mizar, HOL e Coq, presentano gravi carenze nelle loro capacità di esprimere la matematica.
La Mizar Mathematical Library formalizza gran parte della matematica universitaria ed è stata considerata la più grande biblioteca di questo tipo nel 2007.[4] Progetti simili includono il database di dimostrazioni Metamath e la libreria mathlib scritta mediante il software e il linguaggio Lean.[5]
Nel 2014 è stato organizzato il workshop Twenty years of the QED Manifesto[6] nell'ambito della Vienna Summer of Logic.
Note
[modifica | modifica wikitesto]- ^ The QED Manifesto in Automated Deduction - CADE 12, Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994. HTML version
- ^ The QED Workshop II report
- ^ Freek Wiedijk, The QED Manifesto Revisited, 2007
- ^ Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, and J. B. Wells, Gradual Computerisation/Formalisation of Mathematical Texts into Mizar
- ^ mathlib libraryhttps://leanprover-community.github.io/mathlib-overview.html
- ^ Twenty years of the QED Manifesto workshop
Bibliografia
[modifica | modifica wikitesto]- H. Barendregt & F. Wiedijk, The Challenge of Computer Mathematics, Transactions A of the Royal Society 363 no. 1835, 2351–2375, 2005
- A Special Issue on Formal Proof, in Notices of the American Mathematical Society, dicembre 2008. (numero open access)
- Richard A. De Millo, Richard J. Lipton, Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, Volume 22, n. 5 (maggio 1979), pp. 271 - 280
- John Harrison, Formalized Mathematics, Technical Report 36, Turku Centre for Computer Science (TUCS)
- Ittay Weiss, The QED Manifesto after Two Decades ¾ Version 2.0, Journal of Software vol. 11, no. 8, pp. 803-815, 2016.
Collegamenti esterni
[modifica | modifica wikitesto]- Freek Wiedijk, Formalizing 100 Theorems Pagina che tiene traccia dei progressi nella formalizzazione di 100 comuni teoremi.
- Freek Wiedijk, The Seventeen Provers of the World, dimostrazione dell'irrazionalità della radice quadrata di 2 in 70 assistenti della dimostrazione.
- Formalized Mathematics, una rivtsa che presenta le dimostrazioni di Mizar
- The Archive of Formal Proofs un repository di dimostrazioni in Isabelle/HOL.
- [1] Un repository di didimostrazioni in Coq.
- UniMath "la libreria Coq mira a formalizzare un corpo sostanzioso di conoscenze matematiche adotando un punto di vista univalente"
