Finding libraries of formalized mathematics
Metamath has a HUGE chapter-organized archive of formal theorems:

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

Besides that, Freek Wiedijk's QED manifesto is always a good starter for future formalizers. And his list of top 100 formalized theorem is an ever-encouraging source of formalized ideas:

http://www.cs.ru.nl/~freek/100/

At the end of that page, he provides another list of desired but-still-missing formalized theorems. The one that I personally desire, is $\mathrm{IP=PSPACE}$.