Re: [isabelle] "The QED Project"

I think it depends on whether you adopt the proposal in its extreme form or in a limited form. No single formal system suffices for the formalisation of all of mathematics, but well-known systems including higher order logic (which is actually fairly weak) suffice to formalise immense chunks of mathematics. Even if we restrict ourselves to the algebra and analysis typically taught to mathematics undergraduates in the first couple of years, I think the great majority of this material has never been formalised.

On 22 Jan 2009, at 14:57, Freek Wiedijk wrote:

Dear list members,

A few days ago I got the email copied below.  And I don't
very well know what to say to it.  Does anyone here have
a good answer to Arnold's query?

(I'm cross-posting this to a couple of mailing lists.  So my
excuses for the duplication, but I'm really curious whether
there is anything interesting to say to this question.)


Message-ID: <4975CDB4.2010107 at>
Date: Tue, 20 Jan 2009 14:12:20 +0100
From: Arnold Neumaier <Arnold.Neumaier at>
To: Freek Wiedijk <freek at>
Subject: The QED Project


are there still activities related to the QED Project
I am contemplating writing a grant application for something going
in a similar direction, and would like to know about which people to
contact for possible collaboration.

What is your current assessment of what it takes to realize an
updated version of the QED project?

Best wishes,


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.