Manifesto QED
# 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

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. 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.

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:

* 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. Progetti simili includono il database di dimostrazioni Metamath e la libreria mathlib scritta mediante il software e il linguaggio Lean.

Nel 2014 è stato organizzato il workshop Twenty years of the QED Manifesto nell'ambito della Vienna Summer of Logic.

