I would like to mention Mizar, proof verification system based on language which is human readable and very near to natural mathematical language used in mathematical practice. It is one of the longest working proof checkers, and it is one of the most successful one. Here You may find some about it: http://www.cs.ru.nl/~freek/mizar/ There is the whole library congaing presently more that 40Mb zipped proofs ( in pure ascii files!).