Automated proof tools are already causing a headache for mathematicians. The four color theorem was proved by breaking the problem down into 1,936 cases, and th

Automated proof tools are already causing a headache for mathematicians. The four color theorem was proved by breaking the problem down into 1,936 cases, and then proved each of the individually. This story has a happy ending: the result is now fairly well accepted and there have been numerous steps in simplifying the proof. However, other automated proofs have not been so lucky: Hale's proof of the Kepler Conjecture was 300 pages of mathematics and 40,000 lines of supporting computer code, and the referees of the paper tried four years to understand it (they even set up a seminar series for all of the prerequisite material to understand the proof) before letting the authors know that they were unable to verify the correctness of the proof because they "ran out of energy to devote to the problem." (The Annals of Mathematics henceforth edited their rules to disallow submission of computer programs.) The Flyspeck project is to, well, ask a program to verify the correctness of the proof. Ah, the times we live in.