From: Lyle Burkhead (LYBRHED@delphi.com)
Date: Tue Dec 10 1996 - 23:32:03 MST
An article in today's New York Times describes a long-awaited
breakthrough: a computer program has proved a difficult conjecture
that mathematicians have been unable to prove.
The Times does not describe the conjecture (now a theorem) in detail;
it is merely described as the statement that "a set of three equations is
equivalent to a Boolean algebra." It was proposed by Herbert Robbins
in the 1930s. Robbins could not prove his conjecture. He showed it to
Professor Albert Tarski, a well-known logician at Stanford. According
to the article, "Dr. Tarski, who is now dead, worked on the problem,
included it in a book, and handed it out to graduate students and visitors."
In other words, this is not a "toy" problem. It has been worked on by
numerous mathematicians of high ability. However, it is not exactly a
problem in the mainstream of mathematics; it is on the fringe between
mathematics proper and mathematical logic.
Now the theorem has been proved by an automated reasoning program
written by Bill McCune at the Argonne National Laboratory.
According to the Times,
> Finally, on Oct. 2, Dr. McCune gave the Robbins conjecture to
> a new automated reasoning program that he had written called EQP,
> for equational prover. Eight days later, on Oct. 10, the computer
> spewed out a proof. Dr. McCune, a low-key researcher, said he was
> "amazed." Dr. Larry Wos, his supervisor, said "Bill was in heaven."
I used to correspond with these people (there is a list devoted to
automated reasoning), so I know a little more about it than the Times
reports. It should be noted that
1. It is one thing to prove a theorem about Boolean algebra, and
something else to prove a theorem about complex analysis.
2. The program was given a conjecture to prove. The program didn't
think up the conjecture itself.
3. There is nothing recursive about this -- in other words, the programs
don't write the next generation of programs. All programming is done
by humans. Larry Wos, Bill McCune and their colleagues aren't trying
to write programs that write programs. That's not even on their agenda
at this point.
4. Instead of trying to get the program to prove theorems all by itself,
it would be much more useful to build a mathematician's workbench,
i.e. a program that would do the same thing for mathematicians that a
text editor does for programmers, a word processor does for writers,
a CAD program does for engineers, etc. IA instead of AI.
Lyle
This archive was generated by hypermail 2.1.5 : Fri Nov 01 2002 - 14:35:53 MST