QED project
|
|
The QED project was a proposal for a computer-based encyclopedia and database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. The idea for the project arose in 1993, mainly under the impetus of Robert Boyer. The goals of the project were outlined in the "QED manifesto", an open document which evolved over many years with input from many researchers. 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. The project seems to have died in 1996, never having produced more than discussions and plans. However, the Mizar system implements many of the goals set forth in the QED manifesto. Q.E.D. means quod erat demonstrandum in Latin, from Greek oper edei deixai, meaning "that which was to be demonstrated."
External links
- QED project main page (http://www-unix.mcs.anl.gov/qed/), includes a link to the manifesto, conference reports and mailing list archives.