The QED manifesto was a proposal for a computer-based database of all

mathematical Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...

knowledge, strictly formalized and with all proofs having been checked automatically. ( Q.E.D. means in

Latin Latin (, or , ) is a classical language belonging to the Italic branch of the Indo-European languages. Latin was originally a dialect spoken in the lower Tiber area (then known as Latium) around present-day Rome, but through the power of the ...

, meaning "which was to be demonstrated.")

Overview

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 in 1994 at

Argonne National Laboratories Argonne National Laboratory is a science and engineering research national laboratory operated by UChicago Argonne LLC for the United States Department of Energy. The facility is located in Lemont, Illinois, outside of Chicago, and is the larg ...

and the second in 1995 in

Warsaw Warsaw ( pl, Warszawa, ), officially the Capital City of Warsaw,, abbreviation: ''m.st. Warszawa'' is the capital and largest city of Poland. The metropolis stands on the River Vistula in east-central Poland, and its population is officia ...

organized by the

Mizar Mizar is a second-magnitude star in the handle of the Big Dipper asterism in the constellation of Ursa Major. It has the Bayer designation ζ Ursae Majoris ( Latinised as Zeta Ursae Majoris). It forms a well-known naked eye d ...

group. 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. In order of importance: * Very few people are working on formalization of mathematics. There is no compelling application for fully mechanized mathematics. *

Formalized mathematics This article examines the implementation of mathematical concepts in set theory. The implementation of a number of basic mathematical concepts is carried out in parallel in ZFC (the dominant set theory) and in NFU, the version of Quine's New Foun ...

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 assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

s; the paper finds that the major contenders,

, HOL, and

Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof ...

, have serious shortcomings in their abilities to express mathematics. Nonetheless, QED-style projects are regularly proposed. The

Mathematical Library formalizes a large portion of undergraduate mathematics, and was considered the largest such library in 2007. Similar projects include the

Metamath Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in ...

proof database and the mathlib library written in

Lean Lean, leaning or LEAN may refer to: Business practices * Lean thinking, a business methodology adopted in various fields ** Lean construction, an adaption of lean manufacturing principles to the design and construction process ** Lean governm ...

. In 2014 the Twenty years of the QED ManifestoTwenty years of the QED Manifesto workshop
/ref> workshop was organized as part of the

Vienna Summer of Logic The Vienna Summer of Logic was a scientific event in the summer of 2014, combining 12 major conferences and several workshops from the fields of mathematical logic, logic in computer science, and logic in artificial intelligence. The meetings too ...

References

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.

A repository of proofs in Coq.
UniMath
"Coq library aims to formalize a substantial body of mathematics using the univalent point of view" Educational projects Formal methods Mathematics literature Proof assistants

Overview

See also

References

Further reading

External links