another country

Larry Wos <wos>
From: Larry Wos <wos>
Date: Thu, 6 May 93 14:56:28 CDT
Message-id: <9305061956.AA10771@altair.mcs.anl.gov>
To: qed@mcs.anl.gov
Subject: another country
Sender: qed-owner
Precedence: bulk

 
discovery and mathematicians
  
 The following is intended to be for the recent discussion on "discovery"
and the subsequent response to Boyer's comments on the subject.
  
  Regarding the request for mathematicians to comment:
Perhaps I qualify as a mathematician, having gotten my PhD in group theory under
R. Baer, and having done my Masters at the University of Chicago.
My main use of an automated reasoning program for applications is in the
context of proving theorems from areas of mathematics and logic.
With no intended denigration, I refer here to
proof finding, rather than to proof checking.
I consider the former "discovery".
  
  When I hear skepticism regarding the automation of "discovery", first I think
that the skeptic might well have in mind a classical AI approach.
If that is the case, I heartily agree, believing that for countless
decades programs will not function as mathematicians do; nor must they.
The goal of emulating the human mind is certainly not mine, when I
focus on the automation of logical reasoning.
Indeed, I think such emulation a goal essentially out of reach.
For example, the mathematician uses instantiation when deducing that the
square of yz is the identity from the hypothesis that the square of
x is the identity, in the theorem that asserts that groups in which
the square of every element is the identity are cmmutative.
Wise instantiation seems too difficult to automate.
Perhaps behind the negative New York article (July 14 1991) is some
despair at capturing the mathematician's mind in a computer program.
Clearly, the mathematicians they quoted were unaware of the
successes in answering open questions, where a key role was played by an automated reasoning program.
I am in no way talking about a computational role;
instead, I mean arguments of the type found in group theory, ring theory,
various logic calculi, and the like.
That the "formalization of discovery is extremely hard" cannot be doubted.
But, unless one is interested in the "theory" of discovery,
it seems clear to me that we at Argonne have succeeded (in effect)
in formalizing discovery in the sense that our programs do discover marvelous proofs.
  
  That mathematicians use "disparate" and "mysterious" methods of discovery is
true; when I have asked them about how they found a proof,
seldom can they tell me in detail.
In my own work, I freely admit to waking up with a solution to a problem.
However, rather than (as in classical AI) attempting to emulate such
powerful minds (of people), our programs use disparate methods, diverse strategies
and various inference rules.
The explicit use of strategy, I have often said, is but one of the differences
in some of automated reasoning as compared with research by mathematicians.
Prediction:  Within twenty years, some mathematicians will have
formed an impressive team with some automated reasoning program
to answer a number of deep questions.
Mechanizing discovery is not a long way off:  It is here,
if one means the ability to answer open questions with a reasoning program.
But perhaps I have missed the point of the objection.
Perhaps the idea is the mechanization of presenting interesting theorems,
culled from the output of the program, culled by the program itself.
The New York Times was wrong:  Computers do beautiful mathematics,
and I regret that they never acknowledged my rebuttal article.
  
  I do not feel like a child in a candy shop, unable to choose;
rather, I am delighted with OTTER (McCune's) and its predecessors,
amazed at using it successfully to answer unrelated open questions.
I would have predicted in 1970 that such would not occur in my lifetime or career.
I was wrong, and am s pleased.
Just to be explicit, far, far more is needed, but a grand
beginning has occurred, and not merely one with potential.
  
  Larry Wos