Machine Math
beeson@cats.UCSC.EDU
From: beeson@cats.UCSC.EDU
Date: Tue, 20 Apr 93 13:24:30 -0700
Message-id: <9304202024.AA20321@si.ucsc.edu>
To: qed@mcs.anl.gov
Subject: Machine Math
Sender: qed-owner
Precedence: bulk
I would like to make a distinction between two kinds of formal languages
needed for the QED project:
(1) a high-level language in which humans (and possibly machines)
write proofs and read proofs.
(2) a low-level language in which machines write proofs and check proofs
(and possible generate proofs).
These are analogous to high-level programming languages and assembly code.
In the early days of computing, there was only assembly code. Then
high-level languages and compilers were constructed. With regard to formal
proofs, we are still in those early days. I envision a high-level language,
which for want of a better name I am calling "Machine Math", which would
be approximately as hard to learn as a modern programming language; that
is, somewhat harder than TeX, but not much. Ordinary mathematicians
(who are not logicians or computer scientists) could learn it and write
their proofs in it. A "proof compiler", or many different compilers,
could be built to compile Machine Math into (various) low-level
formal languages, for which proof-checkers in turn can be built.
If anything like the scope of Bourbaki is contemplated, the
initial focus of the project must be on the design of Machine Math.
Computers should NOT BE INVOLVED in the first year of experimentation!
(That's a radical thing for me to say, because I've been up to my elbows
in computer code for the last seven years.)
If the project could successfully produce a specification for Machine
Math, and a large number of examples of proofs formalized in Machine Math,
then independent groups of researchers may build compilers into the
low-level logic of their choice, and build proof-checkers, independently
of one another. This strikes me as much more feasible than trying
to build a single computer system with the cooperation of hundreds of
researchers scattered around the globe.
Machine Math must support definitions, theorems, proofs, and
algorithms. One of the issues about which there will be much
discussion is, what are the allowed mechanisms for specifying an
algorithm? A tremendous variety of informal descriptions occurs in
the mathematical literature, and this is probably the most noticeable
place in which Machine Math proofs will have to be "more formal" than
journal proofs are now; algorithms will clearly have to be written in
some more formal way. We might want to consider some extension of
the Mathematica syntax (or a variant) to a more abstract language;
it would help that the Mathematica syntax is already fairly well-known.
Less obvious is the fact that Machine Math must support "theories".
Each piece of mathematics takes place in the context of (one or more)
theories; functions may have different definitions in different theories
for example. The use of theories will be a help, however, in organizing
a large database of mathematical knowledge.
I suggest the following organization of the QED effort:
1. Machine Math language design and specification.
2. Formalization of a sizeable body of mathematics in Machine Math.
3. Specification of low-order logic(s) as target language(s).
4. Construction of Machine Math compiler(s) into the target language(s).
5. Construction of proof-checkers for the target languages.
6. Construction of database software to manipulate a large body of
mathematics in Machine Math form.