The Four Color Theorem and the Computer Mathematics Revolution: A Century-Old Enigma and the Philosophy of Mechanical Proof