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?