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?

  • 1
    $\begingroup$ 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. $\endgroup$ Oct 29 '18 at 16:12

Metamath has a HUGE chapter-organized archive of formal theorems:


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:


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.