Importing proofs in Logipedia boils down to translating proofs into Dedukti. Currently, this is possible for:

• Matita via Krajono
• OpenTheory and HolLight via Holide
• Coq with CoqInE.