[FOM] The QED Manifesto today

[Jesse Alama]

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., 

  http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.117.1046/jordan.html

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

  http://journals.royalsociety.org/

Jesse

-- 
Jesse Alama (alama at stanford.edu)