"Computers and Proof: Applying automated reasoning to prove mathematicaltheorems," by Ivars Peterson. Science News, 22 March 1997, pages176-177.
This article describes a recent proof, produced by a computer, of amathematical conjecture that some of the best mathematicians of this centuryhave tried and failed to prove. The Robbins conjecture, a statement inmathematical logic, was first proposed in the 1930s by Herbert Robbins, who isnow 81 years old and a professor at Rutgers University. William McCune, acomputer scientist at Argonne National Laboratory, wrote the automatedreasoning program that produced the proof of the conjecture. The articlequotes McCune's Argonne colleague Larry Wos as saying: "I was surprised thatthe problem finally yielded to the program because some powerful minds hadtried to solve it and hadn't succeeded." The article examines other ways inwhich such programs might be used.
--- Allyn Jackson