[FOM] The QED Manifesto today

Jesse Alama alama at stanford.edu
Sun Jan 25 20:20:39 EST 2009

Arnold Neumaier <Arnold.Neumaier-4JhlDu4IDl0juwv8T7myQQ at public.gmane.org> writes:

> The QED project for formalizing all of mathematics,
>       http://www-unix.mcs.anl.gov/qed/
> is dead for over a decade. But what happened to the spirit of
> the project? Who works today towards the goals expressed in the
> QED manifesto,
>       http://www.rbjones.com/rbjpub/logic/qedres00.htm
> and how?
> I'd like to ask for your personal opinion on which form such a
> project could/should take when started now.
> I'd also appreciate to get pointers (web sites, pdf, ps) to
>    - people currently active in this direction,
>    - past and current projects towards realizing partial goals,
>    - important papers covering the current state of affairs.

The MIZAR project (http://www.mizar.org), among others, comes close to
achieving the aims of the QED project.  Its language for representing
mathematical knowledge (dependent types, definitions, theorems, proofs,
etc.) is fairly intuitive, its foundational theory (first-order set
theory) is familiar, and its collection of formalized mathematical
knowledge is quite large.  Along with MIZAR there is a journal,
Formalized Mathematics (http://fm.mizar.org/), in which human-readable
versions of MIZAR "articles" are published.  One also has
hyperlinked presentations of mizar articles, e.g., 


on a formalization of a proof of the Jordan curve theorem.

A fairly recent issue of the Philosophical Transactions of the Royal
Society (volume 363, number 1835) contains several articles on isses
closely related to the QED project.  You can get the issue via



Jesse Alama (alama at stanford.edu)

More information about the FOM mailing list