Actually, just converting all the already-known theorems into a form that can be computationally verified (not just convince a skilled human) would be an interesting starting point. This would really help the metamath project, and perhaps make peer review of mathematical research papers easier:

http://us.metamath.org/mpeuni/mmset.html