Computer Use to Computer Proof: A Rational Reconstruction
Thomas Tymoczko · 1981
time there were no computers. Then for a while they were only glorified adding machines. Eventually computers were used in serious practical problems, like solving equations in physics, but they were still slow. We've all heard anecdotes like those told about the Manhattan Project when physicists supposedly raced computers to solve crucial equations-and the physicists won! These anecdotes are like the folk song about John Henry who raced the steam drill and won. Anecdotes and folk songs are fun, but computers and steam drills have come a long way. In any case, physicists do with computers shouldn't matter to mathematicians. In the 1950's computers started to touch on pure mathematics. Logicians programmed computers to prove the early theorems of Principia Mathematica in only a few minutes. Logicians checked the resulting proofs, of course. Later computers must have been used to assist in the discovery of new proofs, but the proofs were traditional proofs; they were still checked by mathematicians. It is easy to imagine a case in which a mathematician so trusts his or her programs that he or she doesn't always bother to check the resulting proofs. It is a short psychological step from such cases to essential computer proofs which can't be examined and verified by mathematicians. Computer use cannot be eliminated from such proofs. The computer does not merely discover a proof which it to the mathematician to check; the computer actually verifies that what it discovered was a proof and it presents to the mathematician is a report that the verification succeeded. Nevertheless computers could have infiltrated this far into mathematics without occasioning much comment. They would be easy to ignore if they were used only to prove esoteric theorems in combinatorics that interested few people beyond the author (probably all of whom were also using computers). What prompts the general question about computers in mathematics is their essential use in proving a simple, long-standing conjecture familiar to all mathematicians. This was accomplished by Appel, Haken and Koch with their now famous computer proof of the