**Mail folder:**QED**Next message:**Zdzislaw Meglicki: "Re: another country"**Previous message:**Zdzislaw Meglicki: "Re: Continuing Conversation - NO Flames"**Reply:**Zdzislaw Meglicki: "Re: another country"

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