Delivery-Date:
From: Larry Wos <wos@mcs.anl.gov>
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@mcs.anl.gov
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