Logipedia

Logipedia is a library of proofs expressed in Dedukti.
Dedukti is a Logical Framework that provides means to define theories such as Predicate logic, Simple type theory, the Calculus of constructions, the Calculus of Inductive Constructions... and to express proofs in these theories.
Within Dedukti, some proofs can be translated from one theory to another.
Some proofs expressed in some Dedukti theories can be translated to other proof systems, such as HOL Light, HOL 4 , Isabelle / HOL , Coq , Matita , Lean , PVS ...
These proofs, originally developed in Matita , has been expressed in a formulation of the Calculus of Inductive Constructions in Dedukti, it has then been translated to a formulation of Simple type theory in Dedukti, and exported to Open theory , Coq , Matita , Lean , and PVS .
You can find more information in the FAQ

Logipedia in a nutshell