"Computers and Proof: Applying automated reasoning to prove mathematical theorems," by Ivars Peterson. Science News, 22 March 1997, pages 176-177.

This article describes a recent proof, produced by a computer, of a mathematical conjecture that some of the best mathematicians of this century have tried and failed to prove. The Robbins conjecture, a statement in mathematical logic, was first proposed in the 1930s by Herbert Robbins, who is now 81 years old and a professor at Rutgers University. William McCune, a computer scientist at Argonne National Laboratory, wrote the automated reasoning program that produced the proof of the conjecture. The article quotes McCune's Argonne colleague Larry Wos as saying: "I was surprised that the problem finally yielded to the program because some powerful minds had tried to solve it and hadn't succeeded." The article examines other ways in which such programs might be used.

--- Allyn Jackson

Return to Top