I don't work in this field, but I would like to know out of lay interest. Are there translators that to convert proofs in one system to another? Such a translator would prove (pardon!) to be useful to collaborating researchers.
I know that these systems each have unique features, so I don't mean a 100% translation. For the purposes of this question, translating proofs for the intersection of features would suffice.
However, it turns out to be non-trivial, so it is not typically done in practice. Formalization requires very precise specification, and even slight differences can cause complications. But like many other things, who knows, perhaps there will be further progress in this area.
I know that these systems each have unique features, so I don't mean a 100% translation. For the purposes of this question, translating proofs for the intersection of features would suffice.