Manifesto QED
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
modificaL'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- ^ 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- 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- 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"
