In response
Larry Wos <wos>
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