*To*: Freek Wiedijk <freek at cs.ru.nl>, Arnold Neumaier <Arnold.Neumaier at univie.ac.at>*Subject*: Re: [isabelle] "The QED Project"*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Fri, 23 Jan 2009 16:49:50 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <95AF5B01-6EA5-4EA2-99F3-2D526A3A3B9D@cam.ac.uk>*References*: <20090122145717.GA5618@auriga.local> <95AF5B01-6EA5-4EA2-99F3-2D526A3A3B9D@cam.ac.uk>

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. Best, Randy -- 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 univie.ac.at> > > Date: Tue, 20 Jan 2009 14:12:20 +0100 > > From: Arnold Neumaier <Arnold.Neumaier at univie.ac.at> > > To: Freek Wiedijk <freek at cs.kun.nl> > > Subject: The QED Project > > > > Freek, > > > > are there still activities related to the QED Project > > http://www-unix.mcs.anl.gov/qed/ > > 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 > > > > http://www.mat.univie.ac.at/~neum/ > > ---------------------------------------------------------------- > > > > > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

**References**:**[isabelle] "The QED Project"***From:*Freek Wiedijk

**Re: [isabelle] "The QED Project"***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] "The QED Project"
- Next by Date: [isabelle] Automata library
- Previous by Thread: Re: [isabelle] "The QED Project"
- Next by Thread: [isabelle] Isabelle document preparation
- Cl-isabelle-users January 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list