Email Gateway (Aug 18 2022 at 12:55): Email Gateway (Aug 18 2022 at 12:55):From: Freek Wiedijk <freek@cs.ru.nl>
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@univie.ac.at>
Email Gateway (Aug 18 2022 at 12:56):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 12:56):From: Randy Pollack <rpollack@inf.ed.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@univie.ac.at>
Date: Tue, 20 Jan 2009 14:12:20 +0100
From: Arnold Neumaier <Arnold.Neumaier@univie.ac.at>
To: Freek Wiedijk <freek@cs.kun.nl>
Subject: The QED ProjectFreek,
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.
Last updated: Nov 21 2024 at 12:39 UTC