"a computer proof of a theorem can run in to the thousands."

For those interested in a small example, look at http://us.metamath.org/mpegif/mmset.html#trivia