This seems overly pessimistic. I'm sure it'd take a lot of work, but consider results like Gonthier's proof of the Odd Order Theorem (see http://research.micro

This seems overly pessimistic. I'm sure it'd take a lot of work, but consider results like Gonthier's proof of the Odd Order Theorem (see http://research.microsoft.com/en-us/news/features/gonthierproof-101112.aspx http://research.microsoft.com/en-us/news/features/gonthierpr...), which formalized a book-length proof.