**Mail folder:**QED**Next message:**Zdzislaw Meglicki: "Machine Math"**Previous message:**jt@linus.mitre.org: "illusiions"**Reply:**Zdzislaw Meglicki: "Machine Math"

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.