A computer program written by researchers at Argonne National Laboratory in Illinois has come up with a major mathematical proof that would have been called creative if a human had thought of it. In doing so, the computer has, for the first time, got a toehold into pure mathematics, a field described by its practitioners as more of an art form than a science. ...Dr. McCune's proof concerns a conjecture that is the very epitome of pure mathematics. ...His computer program proved that a set of three equations is equivalent to a Boolean algebra...
Gina Kolata, "With Major Math Proof, Brute Computers Show Flash of Reasoning Power" The New York Times (Dec 10, 1996)