Re: Boyer's Hypothesis

Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
Message-id: <0fqnwnqKmlE2MUS1dr@arp>
Date: Mon, 26 Apr 1993 11:47:31 +1000 (EST)
From: Zdzislaw Meglicki <Zdzislaw.Meglicki@arp.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Boyer's Hypothesis
Sender: qed-owner
Precedence: bulk
In <9304251444.AA06798@malabar.mitre.org> jt@linus.mitre.org writes:

> If it turns out that the Boyer constant for proofs in these areas [i.e.,
> "real life" mathematics done in the last 30 years] is 10000, then much
> of what we are talking about in this forum about "doing real
> mathematics" is highly speculative and may border on self-deception.

But, this is exactly where systems such as "Analytica" by E. Clarke and
X. Zhao (CMU-CS-92-117) come in. The reason why "real life" mathematical
proofs are so short is because they are not carried out all the way down
to the logical foundations. Instead, they utilize already accumulated
knowledge and prove things by reducing them to other already proven
theorems. The pyramid of structures that has been built in this way over
the last couple of hundred years is very high indeed, but this is also
the most efficient way of doing things: "seeing further by standing on
the shoulders of the giants". The QED system will have to incorporate
somehow this way of doing things if it is at all to be workable and
useful.

In the "Analytica" report you'll find examples of various theorems from
mathematical analysis and their mechanically constructed proofs - the
culmination of the paper is a mechanical proof of Weierstrass' example
of a continuous nowhere differentiable function. The proofs delivered by
the system are short, quite comparable to similar proofs that would be
produced by humans and perfectly readable. So the Boyer constant is
*not* 10,000 in this case: it is about 1. It was possible to achieve
that because the prover was built on the basis of a symbolic computation
system for manipulating mathematical formulas already equipped in a very
formidable data base of mathematical knowledge. 

What QED could add to a system like that would be a sound logical
foundation. I.e., every one of the facts stored in its equally
formidable data base would itself be a theorem with an accompanying
proof. Although the proofs should not go all the way down to the
underlying logic - rather, they should try to reduce problems to already
proven theorems, the way it is done in man-made mathematics - by
combining proofs of theorems on lower levels it should ultimately be
possible to reconstruct mechanically the whole proof tree with its
leaves at the level of the basic logic (although I am not sure why
anybody would ever want to do that - apart from just demonstrating that
it can be done).

   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