Finding libraries of formalized mathematics I want to formalize Interval Newton Methods in Isabelle. As a research, I have the curiosity of whether there is anything done in the field. For that, I need to know what mathematical contents have been formalized in different proof assistants. 

For Isabelle, this is easy: just google the Archive of Formal Proofs. What about the others? Can you help me to complete this list (taken from Wikipedia's table for proof assistants) providing links to the relevant libraries of formalized mathematics:

ACL2 1, Agda, Albatross, Coq, F*, HOL Light, HOL4, Isabelle, Lean, LEGO, Mizar, NuPRL, PVS, Twelf?

If you know of other libraries you are very welcome to add the corresponding tool.

Additions:

Is https://coq.inria.fr/ the primary place to look for proofs written in Coq?
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}$.