QED project
Encyclopedia
The QED manifesto was a proposal for a computer-based database of all mathematical
knowledge, strictly formalized and with all proofs having been checked automatically. (Q.E.D.
means in Latin
, from Greek
(ὅπερ ἔδει δεῖξαι), meaning "that which was to be demonstrated.") The idea for the project arose in 1993, mainly under the impetus of 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. Explicit authorship was deliberately avoided. A dedicated mailing list was created, and two scientific conferences on QED took place. The first one took place in 1994 at Argonne National Laboratories and the second in 1995 in Warsaw
organized by the Mizar group.
The project seems to have died in 1996, never having produced more than discussions and plans. In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project. In order of importance:
Nonetheless, QED-style projects are regularly proposed, and the Mizar
library has successfully formalized a large portion of undergraduate mathematics. it is the largest such library.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
knowledge, strictly formalized and with all proofs having been checked automatically. (Q.E.D.
Q.E.D.
Q.E.D. is an initialism of the Latin phrase , which translates as "which was to be demonstrated". The phrase is traditionally placed in its abbreviated form at the end of a mathematical proof or philosophical argument when what was specified in the enunciation — and in the setting-out —...
means in Latin
Latin
Latin is an Italic language originally spoken in Latium and Ancient Rome. It, along with most European languages, is a descendant of the ancient Proto-Indo-European language. Although it is considered a dead language, a number of scholars and members of the Christian clergy speak it fluently, and...
, from Greek
Greek language
Greek is an independent branch of the Indo-European family of languages. Native to the southern Balkans, it has the longest documented history of any Indo-European language, spanning 34 centuries of written records. Its writing system has been the Greek alphabet for the majority of its history;...
(ὅπερ ἔδει δεῖξαι), meaning "that which was to be demonstrated.") The idea for the project arose in 1993, mainly under the impetus of Robert Boyer
Robert S. Boyer
Robert Stephen Boyer, aka Bob Boyer, is a retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore...
. 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. Explicit authorship was deliberately avoided. A dedicated mailing list was created, and two scientific conferences on QED took place. The first one took place in 1994 at Argonne National Laboratories and the second in 1995 in Warsaw
Warsaw
Warsaw is the capital and largest city of Poland. It is located on the Vistula River, roughly from the Baltic Sea and from the Carpathian Mountains. Its population in 2010 was estimated at 1,716,855 residents with a greater metropolitan area of 2,631,902 residents, making Warsaw the 10th most...
organized by the Mizar group.
The project seems to have died in 1996, never having produced more than discussions and plans. In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project. 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 theorem provers and proof assistants; the paper finds that the major contenders, MizarMizar systemThe Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...
, HOL, and CoqCoqIn computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...
, have serious shortcomings in their abilities to express mathematics.
Nonetheless, QED-style projects are regularly proposed, and the Mizar
Mizar system
The Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...
library has successfully formalized a large portion of undergraduate mathematics. it is the largest such library.
See also
- Formalism (mathematics)Formalism (mathematics)In foundations of mathematics, philosophy of mathematics, and philosophy of logic, formalism is a theory that holds that statements of mathematics and logic can be thought of as statements about the consequences of certain string manipulation rules....
- Mathematical knowledge managementMathematical knowledge managementMathematical knowledge management is the study of how society can effectively make use of the vast and growing literature on mathematics. It studies approaches such as databases of mathematical knowledge, automated processing of formulae and the use of semantic information, and artificial...
- POPLmark, a more modest project in programming language theoryProgramming language theoryProgramming language theory is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting...
Further reading
- H. Barendregt & F. Wiedijk, The Challenge of Computer Mathematics, Transactions A of the Royal Society 363 no. 1835, 2351-2375, 2005 (open access issue)
- Richard A. De MilloRichard DeMilloRichard Allan DeMillo is an American computer scientist, educator and executive. He is currently Distinguished Professor of Computing and Professor of Management at the Georgia Institute of Technology. In June 2008, he announced his intention to step down as the John P...
, Richard J. LiptonRichard J. LiptonRichard Jay "Dick" Lipton is an American computer scientist who has worked in computer science theory, cryptography, and DNA computing. Lipton is presently Associate Dean of Research, Professor, and the Frederick G...
, Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACMCommunications of the ACMCommunications of the ACM is the flagship monthly journal of the Association for Computing Machinery . First published in 1957, CACM is sent to all ACM members, currently numbering about 80,000. The articles are intended for readers with backgrounds in all areas of computer science and information...
, Volume 22, Issue 5 (May 1979), Pages: 271 - 280 - John Harrison, Formalized Mathematics, Technical Report 36, Turku Centre for Computer ScienceTurku Centre for Computer ScienceTurku Centre for Computer Science is a joint department of University of Turku and Åbo Akademi University. TUCS was founded on March 21, 1994 by the aforementioned two universities, and Turku School of Economics, which then was a university of its own...
(TUCS)
External links
- Freek Wiedijk, Formalizing 100 Theorems A page keeping track of the progress in the formalization of 100 common theorems.
- Freek Wiedijk, The Seventeen Provers of the World, a proof of the irrationality of the square root of two in seventeen different proof assistants.
- Formalized Mathematics a journal in which Mizar proofs are presented.
- The Archive of Formal Proofs a similar (refereed) repository of proofs in Isabelle/HOL.
- Metamath Proof explorer a repository of mathematical theorems along with their proofs using the MetamathMetamathMetamath is a computer-assisted proof checker. It has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas...
proof assistant.