[FOM] The QED Manifesto today

[Harvey Friedman]

Here are some interesting and useful references you may want to look at:

http://www.cs.ru.nl/~freek/comparison/
H. Barendregt & F. Wiedijk, "The Challenge of Computer Mathematics",  
Transactions A of the Royal Society 363 no. 1835, 2351-2375, 2005

Notices of the AMS Volume 55, Number 11

A formally verified proof of the prime number theorem
Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff, ACM  
Transactions on Computational Logic, 9(1:2):1-23, 2007

http://www.andrew.cmu.edu/user/avigad/isabelle/

Harvey Friedman

On Jan 22, 2009, at 4:48 AM, Arnold Neumaier wrote:

>
> 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.
>
>
> Arnold Neumaier
> http://www.mat.univie.ac.at/~neum/
>