Machine Math

From: beeson@cats.UCSC.EDU
Date: Tue, 20 Apr 93 13:24:30 -0700
Message-id: <>
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.