"With Major Math Proof, Brute Computers Show Flash of Reasoning Power" byGina Kolata. New York Times, 10 December 1996.
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. His colleague,Larry Wos, called the fact that the computer could solve such a problem "a sign of power, ofreasoning power." The article discusses speculation that such programs mightfundamentally change how mathematics is done.