The QED Project


The aim of the QED project is to build a single, distributed, computerized repository that rigorously represents all important, established mathematical knowledge. The construction of this system will be a scientific undertaking of significant proportions, requiring the cooperation of many mathematicians, computer scientists, research groups, research agencies, universities, and corporations. This system will have benefits for mathematics, science, technology, and education.

The QED Project is described in detail in the QED Manifesto, which is available in plain text and html.

Mailing List

The QED mailing list is To join the list, e-mail with the single line
subscribe qed
as the body of the message. The (hypermail) archives of the mailing list are in several volumes (with a gap, and not up to date).

Additional QED-related Pages

The QED Workshop I, Argonne, 1994

The Workshop was held at Argonne in May of 1994. A report on what happened is available here, with a list of participants.

  • ONR Reference 5000 - 1133/93/A0068
  • Office of Naval Research R and T 4331018srp01
  • Organizers:

  • Robert Boyer, University of Texas
  • Ewing Lusk, Argonne National Laboratory
  • The original proposal is here.

    The QED Workshop II, Warsaw, 1995

    The workshop was under the auspices of the State Committee for Scientific Research (Poland) - grant OGT 42/95, supported by special funding from the Office of Naval Research (USA) under ONR Order No. N00014-95-M-0072, cosponsored by Microsoft (Poland) and the Mizar Users Group.

    Robert Boyer (CLInc.) and Andrzej Trybulec (Warsaw University) were responsible for the scientific programme, with Roman Matuszewski (Warsaw University) being the workshop chairman.

    The final report you can find as:

    Whole report:
    LaTeX version - 108kB, compressed LaTeX - 38kB,
    postscript version - 300kB, compressed postscript - 114kB.
    Report classified by authors (in LaTeX and postscript).

    [Agenda | Participants | Statements]