Editing QED manifesto (section)

==Overview==
The idea for the project arose in 1993, mainly under the impetus of [[Robert S. Boyer|Robert Boyer]]. The goals of the project, tentatively named ''QED project'' or ''project QED'', were outlined in the QED manifesto, a document first published in 1994, with input from several researchers.<ref>[http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/wiedijk_2.pdf The QED Manifesto] in ''Automated Deduction - CADE 12'', Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994. [https://www.cs.ru.nl/~freek/qed/qed.html HTML version]</ref> Explicit authorship was deliberately avoided. A dedicated mailing list was created, and two scientific conferences on QED took place, the first one in 1994 at [[Argonne National Laboratories]] and the second in 1995 in [[Warsaw]] organized by the [[Mizar system|Mizar]] group.<ref>[http://mizar.org/people/romat/qed95rep.pdf The QED Workshop II report]</ref>

The project seems to have dissolved by 1996, never having produced more than discussions and plans. In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project.<ref>Freek Wiedijk, [http://mizar.org/trybulec65/8.pdf The QED Manifesto Revisited], 2007</ref> In order of importance:
* Very few people are working on formalization of mathematics. There is no compelling application for fully mechanized mathematics.
* [[Formalized mathematics]] does not yet resemble real, traditional mathematics. This is partly due to the complexity of mathematical notation, and partly to the limitations of existing [[Automated theorem prover|theorem provers]] and [[proof assistant]]s; the paper finds that the major contenders, [[Mizar system|Mizar]], [[HOL theorem prover family|HOL]], and [[Coq (software)|Coq]], have serious shortcomings in their abilities to express mathematics.

Nonetheless, QED-style projects are regularly proposed.  The [[Mizar system|Mizar]] Mathematical Library formalizes a large portion of undergraduate mathematics, and was considered the largest such library in 2007.<ref>Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, and J. B. Wells, ''[http://mizar.org/trybulec65/7.pdf Gradual Computerisation/Formalisation of Mathematical Texts into Mizar]''</ref>  Similar projects include the [[Metamath]] proof database and the mathlib library written in [[Lean (proof assistant)|Lean]].<ref>mathlib library''https://leanprover-community.github.io/mathlib-overview.html''</ref>  

In 2014 the Twenty years of the QED Manifesto<ref>[https://www.cs.ru.nl/qed20/QED-index.html Twenty years of the QED Manifesto workshop]</ref> workshop was organized as part of the [[Vienna Summer of Logic]].