> 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.
I see nothing in this to ensure that the formal system used is consistent.
It is fine to leave the choice of whether or not to accept a formal system
to a logician or degree-level mathematician, but it is unlikely that some
other users (e.g., high school students?) would be able to make an informed
decision about this. It might be a good idea, therefore, to have certified
and uncertified formal systems. A certified system would have been approved
by a group of experts to be a `trustworthy' or `widely-accepted' system.
The tools made available to the general public for accessing the database
might only allow theorems associated with certified systems to be used, or
would at least give a very clear warning if the user tries to exploit a
result in an uncertified system.
> (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.)
It might be useful to allow references to standard text books, etc., to be
stored with a proof, not only to assist the user, but it might also help in
finding duplicates if tidying up of the library is ever required.
Now for some suggestions:
It seems to me that QED has to be distributed, not only in human effort,
but also in terms of where the data is stored. Can we make use of the
World Wide Web? One can envisage having a QED browser much like the HTML
browsers used for hypertext. Maybe the existing browsers can be used?
I envisage that anyone could make their proofs available on The Web without
any authorisation, but to be included in the official QED library the proof
would have to be registered at one of a small number of sites (one or two
on each continent). The contributor might send a request for a proof to be
included, specifying only the hyperlink. A program at the official site
could then follow the link, check the proof, and if acceptable include the
link in the index (or whatever) of the QED library. It would then inform
the other official sites of the new entry. As usage grows the number of
official sites might have to become quite large so as not to overload any
one site with users accessing the library.
So, how about we begin by developing a language/format for specifying
proof systems and proofs? The subscribers to this list could then,
if they wish, write programs to put theorems from their favourite prover
into the QED format. There are bound to be many inadequacies with the
first attempt at the format; testing it with the various proof systems
and libraries of theorems already in use should iron-out a lot of them.
We might then be in a position to write some library-accessing tools,
having real data to test them on. If the idea seemed to be working the next
stage would be to start building a real QED library.
Having a standard interface format for theorem provers has applications
outside of QED and is something that funding could probably be obtained
for fairly easily.
Richard Boulton
University of Cambridge Computer Laboratory