In 1976, Kenneth Appel and Wolfgang Haken, two mathematicians at the University of Illinois, announced to the world that they had found a proof of the famous Four-Color Problem: can every map be colored with four colors so that adjacent countries are assigned different colors? Having a solution to this simply stated problem, which had stumped the mathematical community for one hundred years, was news enough. But the really shocking aspect of the announcement was that the mathematicians had used a computer to do the really hard parts. In fact, their proof could not even be checked without a computer! Needless to say, this was fundamentally troubling to many in the mathematical community. As Ron Graham, a mathematician at Bell Labs, wondered, "The real question is this: If no human being can ever hope to check a proof, is it really a proof?"