# 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.

Is https://coq.inria.fr/ the primary place to look for proofs written in Coq?

• To check Coq libraries, you can take a look at this (incomplete) opam repository of packages: coq.io/opam. You can also find some more libraries on GitHub using coq tag. – Anton Trunov Oct 29 '18 at 16:12

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}$$.