Delivery-Date: 
Message-Id: <kfmXWBeKmlE24xcJwf@arp>
Date: Tue, 13 Apr 1993 13:50:37 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@au.edu.anu.arp>
To: qed@gov.anl.mcs
Subject: QED, Bourbaki and Mathematica
Sender: qed-owner@gov.anl.mcs
Precedence: bulk

I've read the manifesto with great interest. The idea is indeed fitting
the end of this Century. Much like Hilbert, Russell, and Bourbaki
programs before, it attempts to build up Mathematics from the scratch
using formal methods. The difference is that this time the methods will
be based on computer reasoning. The task, as the authors of the
Manifesto readily admit is enormous (I am tempted to refer to it as
"Computer Science Superconducting Supercollider"). 

I'd like to add my 2 pennies to some of the issues brought up by the Manifesto:

> Objection 7.  Good mathematicians will never agree to work with formal
> systems because they are syntactically so constricting as to be
> inconsistent with creativity.

Many mathematicians I know just love using Mathematica and some other
similar systems. Although not as constricting as formal systems they
force the users to adopt unnatural notation (because how else can you
type all this stuff in) and, if the users want to carry out any symbolic
reasoning, enforce a formal language of some kind (most commonly based
on rewriting rules - like Mathematica). As has been recently
demonstrated by Clarke and Zhao such an environment can be used to
produce a surprisingly powerful theorem prover readily applicable to
real life mathematics ("Analytica - A Theorem Prover for Mathematica",
E. Clarke and X. Zhao, CMU-CS-92-117, September 1992). 

Clarke and Zhao have rightly, I think, drawn attention in their
Introduction to the fact that a large amount of domain knowledge is
required for even the simplest proofs in Mathematical Analysis.
Presumably, in the case of the QED project even this domain knowledge
would have been properly derived and proven. Yet, once proven, it's got
to be stored and used in a way that is similar to the current generation
of symbolic manipulation systems. Hence an efficient data base look up
is likely to be a very important aspect of the project. It is also
likely to add to the size of the system. 

The interface is a very important issue too. The technology nowadays is
sufficiently advanced to allow mathematicians the use of real
mathematical notation. It should not be necessary to type "\int" for an
integral: an appropriate integral icon should be available and draggable
onto the workspace. A sophisticated parser should be written which would
scan the workspace and make sense of what's there. A system like that
could become very attractive not only to the retired mathematicians (I
wouldn't be surprised if a high death rate amongst QED contributors
would alarm appropriate health authorities in the US and elsewhere), but
also to people actively working at the frontiers of mathematics. The
design of such a "graphical" intelligent parser could become an
important sub-project in its own right. Once implemented it would open
the system to numerous contributions from active mathematicians. 

Last but not least, what language is it to be written in? Lisp, Haskell,
SML, C, Mathematica? Perhaps a new special language should be
constructed for this work in the first place?

The three issues mentioned above: knowledge data base, user interface,
and language seem to me to be quite fundamental to the project. Is a
consensus likely to be found on any of those? If a project like that was
to be contributed by numerous sites who would coordinate it?

   Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au,
   Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS,
   The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, 
   Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158