[FOM] The QED Manifesto today
friedman at math.ohio-state.edu
Fri Jan 23 07:41:50 EST 2009
Here are some interesting and useful references you may want to look at:
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
On Jan 22, 2009, at 4:48 AM, Arnold Neumaier wrote:
> The QED project for formalizing all of mathematics,
> 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,
> 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
More information about the FOM