Re: [isabelle] "The QED Project"

If the question is "what to suggest to Arnold Neumaier", here is my
suggestion: work on specific project(s) while keeping dreams of large
scale formalized textbook mathematics in mind for the future.

There are projects on formalizing specific mathematics, such as
Flyspeck, clearly inspiring and useful for the long term goal of
formal mathematics.  Equally, much tool development needs doing before
large scale textbook mathematics is feasibly formalizable: large scale
libraries, search, cooperative working (like a WIKI).  Much to do in
automation, decision procedures, ...  Even syntax notations in
existing tools are inadequate for really large scale formalization.
Foundations: as Larry said, HOL *suffices* to formalize immense chunks
of mathematics, but that doesn't mean that it is the right choice.
HOL (as we know it) could use more polymorphism.  HOL suffices, but is
not convenient, when you want to do induction over the height of
derivations of some inductively defined relation.  Modularity in HOL
is (at best) second class.  Binding: nominal Isabelle is a great tool,
but I wouldn't say that formalization of binding is a done deal.  And
so forth.  Many of these suggestions offer possibilities for
collaboration, such as Flyspeck.

Lawrence Paulson writes:
 > 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.
 > Larry
 > 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.)
 > >
 > > Freek
 > >
 > > ----------------------------------------------------------------
 > > 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
 > >
 > > Freek,
 > >
 > > 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,
 > >
 > > Arnold
 > >
 > >
 > > ----------------------------------------------------------------
 > >

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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