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