You can also add Coq's to the mix: [3] https://coq.inria.fr/library/ https://coq.inria.fr/library/ Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq

You can also add Coq's to the mix: [3] https://coq.inria.fr/library/ https://coq.inria.fr/library/ Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq respectively). Logipedia too, is using the language Dedukti, although it is designed to translate into other proof languages, and list these on Logipedia.