Editing QED manifesto

{{Short description|Proposal for a computer-based database of all mathematical knowledge}}
The '''QED manifesto''' was a proposal for a computer-based database of all [[mathematics|mathematical]] knowledge, strictly formalized and with all proofs having been [[automated proof checking|checked automatically]]. ([[Q.E.D.]] means {{lang|la|quod erat demonstrandum}} in [[Latin]], meaning "which was to be demonstrated.")

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

==See also==
* [[Formalism (mathematics)]]
* [[Mathematical knowledge management]]
* [[POPLmark]], a more modest project in [[programming language theory]]

==References==
{{Reflist|30em}}

==Further reading==
* [[H. Barendregt]] & F. Wiedijk, ''[https://www.cs.ru.nl/~freek/notes/RSpaper.pdf The Challenge of Computer Mathematics]'', Transactions A of the Royal Society 363 no. 1835, 2351–2375, 2005
*{{cite web|title=A Special Issue on Formal Proof|url=https://www.ams.org/notices/200811/|work=Notices of the American Mathematical Society|date=December 2008}} (open access issue)
* [[Richard DeMillo|Richard A. De Millo]], [[Richard J. Lipton]], [[Alan J. Perlis]], ''[http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf Social processes and proofs of theorems and programs]'', ''[[Communications of the ACM]]'', Volume 22, Issue 5  (May 1979), Pages: 271 - 280<!-- this paper is actually more relevant today for its comments on mathematical proofs rather than its (doomsday) predictions on the failure of program verification -->
* John Harrison, ''[http://www.cl.cam.ac.uk/~jrh13/papers/form-math3.html Formalized Mathematics]'', Technical Report 36, [[Turku Centre for Computer Science]] (TUCS)
* Ittay Weiss, ''[http://www.jsoftware.us/vol11/185-ID55.pdf The QED Manifesto after Two Decades  Version 2.0]'', ''Journal of Software'' vol. 11, no. 8, pp. 803-815, 2016.

==External links==
* Freek Wiedijk, [https://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems] A page keeping track of the progress in the formalization of 100 common theorems.
* Freek Wiedijk, [https://www.cs.ru.nl/~freek/comparison/ The Seventeen Provers of the World], a proof of the [[Square root of 2#Proofs of irrationality|irrationality of the square root of two]] in seventeen different proof assistants.
* [http://fm.mizar.org/ Formalized Mathematics] a journal in which Mizar proofs are presented.
* [http://afp.sourceforge.net/ The Archive of Formal Proofs] a similar (refereed) repository of proofs in Isabelle/HOL.
* [https://coq.inria.fr/opam/www/ ] A repository of proofs in Coq.
* [https://github.com/UniMath/UniMath UniMath] "Coq library aims to formalize a substantial body of mathematics using the [[Univalent foundations|univalent]] point of view"

[[Category:Educational projects]]
[[Category:Formal methods]]
[[Category:Mathematics literature]]
[[Category:Proof assistants]]