Thoughts on QED

Thursday, 11 August 1994 16:32:01 EDT

Here is a more complete discussion of the ideas about QED
which I discussed at CADE. You'll probably also get a copy of this
from the QED mailing list.

First of all, I am strongly in agreement with those who
feel that QED is an important and worthwhile project. Of course,
there is room for lots of discussion and disagreement about various
details of the QED project.
The QED project may have many facets, but it seems clear that
at the heart of it will be some sort of machine-readable library of
theorems whose proofs have been verified by machine. In chapter 4 of
the QED Manifesto there is extensive discussion of the planning that
must be done and the need for choosing appropriate languages, proof
systems, definitions, ways of organizing the library, etc. One may be
led to despair when one thinks seriously about the prospects for
achieving consensus on all of these matters. The point I would like to
make is that while these matters are important and deserve careful
consideration from many perspectives, fruitful work on the QED project
can commence without waiting for these questions to be settled,
and a useful QED universal library of theorems and proofs is possible
even if general consensus is never reached on some of these matters.
I envision the QED library as a vast database and a large
number of associated utilities for accessing, displaying, translating,
manipulating, and using the items in the database in many ways.
Since it will be difficult or impossible to obtain universal
agreement on the choice of a formal language, definitions and terminology,
and proof systems, I propose that the QED library permit great variety
in such matters. Each item in the library would consist of some
representation of a theorem and a proof for the theorem, along with
information which would specify precisely the formal language,
definitions and terminology, postulates (theory), lemmas, and proof
system which were used in stating and proving the theorem.
Any person or group could register a proof system (which would
include a formal language and a specification of how theorems and
proofs are to be represented) with the QED library. Part of the
registration process would be to provide a program which would check
whether alleged proofs in that proof system really are proofs (and
whether all the associated information mentioned above has been
provided). Thereafter, anyone could submit a theorem and proof in
that proof system to the library, and those that satisfied the
proof-checking program would be added as items in the library.
(Eventually there may be a need to avoid cluttering the library with
trivialities, or trivial variants of items already stored, but that is
a separate issue beyond the scope of this discussion.) Of course,
those who regarded a particular proof system or proof-checking program
as inappropriate or unreliable could avoid using such library items in
their work.
Having the library include items involving many different
proof systems would certainly make it more complicated than would be
the case if there were just one proof system, but the diversity of
our intellectual world is a fact of life, and a library of theorems
which allowed only one proof system would contain only a part of
what should ultimately be available in a universal library. It seems
best to allow in principle for great diversity, and then see how
many proof systems people actually register with the library, and
which ones are actually used extensively. There is a natural process
of evolution in mathematical formalisms, and perhaps eventually there
will be only one formalism which anyone actually uses. Rather than
trying to predict now what that will be, it seems best to organize
the library in a way which will permit the evolutionary process to
progress naturally.
Of course, theorems and proofs can sometimes be translated
from one proof system to another. We may hope that much research on
the relationships between proof systems will be stimulated by the QED
project, and that programs based on the results of this research will
be developed as utilities for coping with the diversity of proof
systems used in the library.
Let us consider the problem of classifying and organizing the
information in the library. Obviously, this is a complex task which
needs to be approached with care and imagination, and one can imagine
endless arguments about how it should be done. However, in this
context a classification scheme is basically a program for accessing
and displaying the raw data, and there is no reason a number of
different classification programs should not coexist as QED utilities.
People could use whichever one they liked best. Thus, it might be
best for the raw library items to be labeled in an neutral way (such
as with the date and time of entry into the QED library), and each
classification scheme could have its own names for theorems and an
index relating these names to the labels of items in the library.
Similarly, there need not be agreement on the style or notation
in which theorems and proofs are presented. There can be a variety of
programs which operate on the raw data in the library to produce
a display congenial to the user.
Of course, decisions about proof systems, notations,
classification systems, etc., will still have to be considered
carefully by the people who develop these systems, and we may hope
that careful consideration will lead to the development of some very
good systems which many people will wish to use. However, I hope I
have made it clear that we need not have general agreement on these
decisions in order to have a useful QED library. The library can
start growing as soon as some basic procedures for registering proof
systems and entering items in the library have been established. As
the library database grows, it will become an increasingly useful
testbed for the development of QED utilities, and these utilities will
in turn make the library more useful, and stimulate its growth.