**Mail folder:**QED**Next message:**LYBRHED@delphi.com: "How many false theorems are there?"**Previous message:**Zdzislaw Meglicki: "Re: another country"

From: Larry Wos <wos> Date: Fri, 7 May 93 08:59:10 CDT Message-id: <9305071359.AA13647@altair.mcs.anl.gov> To: qed@mcs.anl.gov Subject: In response Sender: qed-owner Precedence: bulk

In response to various queries, I enclose first an article from the New York Times, and second my rebuttal article, which they never acknowledged. Computers Still Can't Do Beautiful Mathematics - by Gina Kolata Week in Review Section E, Sunday, July 14, 1991 p. 4- Mathematicians often say that their craft is as much an art as a science. But as more and more researchers are using computers to prove their theorems, some worry that the magic is in danger of fading away. In the past, mathematicians could count on being able to sit down with a newly published proof and carefully follow the researcher's logic, determining whether the derivations held true, relishing particularly clean and clever arguments. But when a computer is used to help prove a conjecture, reasoning is often replaced by calculation. Instead of converging on an answer through a long chain of logical deduction, mathematicians now often use computers to systematically test and discard a vast number of possible answers until they hit on the right one. Dr. Daniet Kleitman, a mathematician at MIT, explained why many mathematicians shrink back from this experimental approach. "One's motivation for reading a paper is not only to become aware of the results, but also to understand how such a proof is formulated and how it actually works," he said. "The question is, Do you want to have an experimental mathematics? Do you want to make traditional papers into experimental things?" Many mathematicians object to being put in a position of having to trust a computer and the assumptions made by its programmer. In a sense, the program itself becomes a part of the proof, and few mathematicians are equipped to check its reliability. In May Dr. Fan R. K. Chung, the editor of the Journal of Graph Theory, decided she was getting so many computer-aided proofs that it was time to formulate a policy. She wrote to her 20-member editorial board, providing one newly received paper as a test case. "Is an important result with a computer-assisted proof acceptable?" she asked. If so, "how should the paper be evaluated knowing that it is almost impossible for the referee to verify its correctness?" The paper that Dr. Chung chose as an example was submitted by Dr. Brendan McKay of the Australian National University and Dr. Stanislaw P. Radiszzowski of the Rochester Institute of Technology. It solved a variant of what mathematicians call the party problem: What is the minimum number of people you have to invite to a party to be sure that, among them, there are eight people or more who all know one another or three people or more who are all strangers to one another? The answer, discovered after some marathon computer crunching, is 28. A classical proof would have demonstrated through an unassailable chain of logic that the answer could only be 28. Instead, Dr. McKAy and Dr. Radiszowski took an experimental approach. Even with a computer, it would be impossible to examine the myriad ways--10 followed by 112 zeroes--that 28 party-goers could be acquainted with one another. But using some clever mathematics, Dr. McKay and Dr. Radiszowski cut down the number of calculations to a mere 100 trillion and then automatically sifted through permutation after permutation, ruling out all gatherings smaller than 28. In the end, the method gave an answer, but did not show why the answer was what it was. And it could not be generalized to solve other party problems. Computer-aided proofs have been a festering problem in mathematics for 14 years, ever since a famous conjecture, the four-color problem, was solved. The problem asked whether any arbitrary map of real or invented countries could be colored, as was generally believed, with four or fewer different colors. No two adjacent countries could be colored the same. In 1977, Dr. Kenneth Appel and Dr. Wolfgang Haken of the University of Illinois published a paper proving that four colors were indeed enough. But the 100-page proof relied on extensive computer calculations. The mathematicians argued that all possible maps could be boiled down to 2,000 standard configurations and then proved, by trying different colorings, that each of those 2,000 maps could be colored in four or fewer hues. "It was a very routine type of calculation that was just repetitive," Dr. Appel said. Many mathematicians found the proof difficult to swallow. It revealed no deep mathematical truths and provided no techniques that could help with other problems. "It is such a nasty situation," Dr. Chung said. "A lot of people just reject the proof outright. It goes against the instincts of most mathematicians." In their replies to Dr. Chung, many members of her editorial board expressed their hesitation about embracing such proofs. Dr. Frank Harary of New Mexico State University wrote that the proof should be "fully verified as correct by an independent computing organization" before the journal considers it. Then, if it accepts the paper, it should publish only the result, he said, while the proof should appear in a computer journal. Dr. Gary Chartrand of Western Michigan University suggested that the result could be published in a special section, titled something like "Research Announcement," taking care to mention that the proof had not been verified. Several others, like Dr. Noga Alon of Tel Aviv University, suggested that the journal accept only papers on "important" theorems and then require the authors to submit a copy of their program, so it could be available to others if they wanted to examine it. In the end Dr. Chung decided to accept the paper., But she decided not to ask for the program. "I don't think the journal should be held accountable," she said. "I think computer-aided proofs are a trend we cannot ignore. But we have to weigh them. If it is a computer-assisted proof, it is a minus. If it is a classical problem, it is a plus." While computer-aided proofs may be published as mileposts on the way to solving a problem, many mathematicians won't consider the problem really solved until there is a proof-- even if it is a hundred or more pages long--that a lone human sitting in a room can go through line by line and understand. Computers Do Produce Beautiful Mathematics Dr. Larry Wos Mathematics and Computer Science Division Argonne National Laboratory Computers do produce beautiful mathematics. In drawing the opposite conclusion, the July 14 article published in the ``Week in Review'' section overlooked the entire field of automated reasoning. The science and art so evident in the research of mathematicians are now complemented by the assistance provided by a new type of computer program that reasons logically. The field whose research has culminated in the design of such programs is called automated reasoning. Rather than simply calculating what is needed to examine a myriad of possibilities, automated reasoning programs now produce proofs that are sequences of logical steps, each step drawn from earlier steps. Indeed, what makes the results provided by a computer so satisfying is that they include the history of the steps of which the result consists. Thus a mathematician can sit alone in an office and enjoy results that share the magic often found in publications in which computers play no role. Further, the mathematician can quickly learn how the proof works, often generalize the approach taken, sometimes encountering deep mathematical truths, and without the need to trust the program that produced the proof. In addition to exhibiting logical reasoning of the type found in mathematics, reasoning programs produce results that are startling and elegant. Dr. J. Lukasiewicz was well recognized for his contributions to areas of logic, and yet the program OTTER recently found a proof far shorter and more elegant than that produced by this eminent researcher, and the program used the same notation and style of reasoning. Mathematicians and logicians find elegance in shorter proofs. Indeed, mathematicians of note are more than interested in what might be done with an automated reasoning program. Dr. I. J. Kaplansky of the University of California at Berkeley once suggested an open question for study by the computer. That question was answered, and answered by reasoning and not by calculation. Dr. John Kalman of the University of Auckland posed a number of questions concerning possible axioms for a field in logic. Contrary to the conjecture that each of the formulas under study was too weak, a computer program provided a complicated and lengthy proof showing that two of them offer the needed and sought-after power. The proofs are precisely in the style that Kalman used in some of his published papers, offering a line of logical thought that could be checked for accuracy. Knowing that a reasoning program can produce such proofs, a scientist might wish to have a personal copy of such a program. That wish is easy to satisfy. Some reasoning programs run well on workstations, on personal computers, and on the Macintosh. Evidence of how well such programs run is provided by the following occurrence. In August of 1990, Dr. Dana Scott of Carnegie Mellon University attended a workshop at Argonne National Laboratory. There he learned of OTTER and some of its uses and successes. Upon returning to his university, Dr. Scott's curiosity prompted him to suggest (via electronic mail) 68 theorems for consideration by the computer. His curiosity was almost immediately satisfied, for the sought- after 68 proofs were returned with the comment that all were obtained in a single computer run with the program--and in less than 16 CPU minutes on a Sun 4 workstation. Dr. Scott now uses his own copy of OTTER on his Macintosh. The type of program that has produced these results and that we expect will continue to do so is in no way a replacement for the mathematician or logician. Nor will it ever be. Instead, this type of program provides an automated reasoning assistant whose work and methods complement those of the scientist. Reasoning assistants like OTTER are not designed in the classical notion of artificial intelligence; these programs do not take an approach that a person would take. Quite the reverse, for automated reasoning programs rely on techniques and procedures that a person would prefer not to use. Nevertheless, their use has resulted in answers to questions that were and are of interest to experts in various fields. Dr. R. Smullyan of the University of Indiana showed great pleasure and surprise at learning of some of the successes achieved by an automated reasoning program. As evidence of his interest, he posed a number of questions, receiving in turn the answers to all but one of them--a question that is still open. Without the following features, so evident in the program OTTER, far less beauty and elegance would have been produced by a program reasoning logically. This newest reasoning program, designed by Dr. William McCune of Argonne National Laboratory, can be instructed to seek shorter proofs. Such proofs are cited by Dr. E. Dijkstra of the University of Texas as important to proving the correctness of computer programs. OTTER can be given hints and suggestions based on the researcher's knowledge and intuition. The program can be instructed to seek one, two, or as many proofs as the allotted time allows, and then present each of the proofs with enough detail to permit checking for accuracy. What makes this program of particular appeal is its use of strategy, one type to restrict its reasoning, and one type to direct it. Rather than detracting from the beauty, elegance, and even magic of mathematics and logic, the use of a computer program--especially a reasoning program--can add to each. It has already. Some of the proofs found with such a program have been published in journals well respected by scientists, for example, the Journal of Algebra and the Notre Dame Journal of Formal Logic. Those proofs are logical in structure, not ones of computation. When I was a student in the Mathematics Department at the University of Chicago almost four decades ago, I would have thought it impossible for a computer to provide such proofs. After all, computers were to be used for calculations, mainly of a numerical character, not for logical reasoning. However, as it turns out, computer programs do reason, and reason so effectively that open questions are sometimes answered. Indeed, in my role as mathematician, I constantly use such a program (OTTER) in my own research. As for the difference of opinion expressed here and in the article published in the New York Times on July 14, the most probable explanation is the simplest: Most likely the scientists quoted in the article have no acquaintance with the program OTTER and with the successes obtained with it. Clearly, the enthusiasm of Dr. Scott, Dr. Smullyan, Dr. Kalman, and Dr. Kaplansky must be well placed. When I once asked Dr. Kaplansky about the automation of reasoning in the context of proving theorems, he replied, "You have a friend in court. Should you continue in your research, the mathematics papers written in 2060 or thereabouts will be at a new level of reading, with much of the current level within reach of a theorem-proving program." The beauty and magic of mathematics will never die, or even lessen. A proof consisting of a sequence of steps, each obtained by applying logical reasoning, is a marvel-- whether produced by a person or produced by a computer! Larry Wos