May be tangential, but take a look at the Mizar project [1]. It has a huge repository of around 50k machine verified non-trivial theorems in human readable syntax (e.g. Gödel's completeness theorem for first-order logic).

Also check out the journal Formalized Mathematics [2]. The idea is that every major new theorem in a paper has a machine verified proof attached.

[1] http://mizar.uwb.edu.pl

[2] http://mizar.uwb.edu.pl/fm/