There has been some work to translate between systems. For example, see "Conversion of HOL Light proofs into Metamath" by Mario Carneiro, 2014: https://arxiv.o

There has been some work to translate between systems. For example, see "Conversion of HOL Light proofs into Metamath" by Mario Carneiro, 2014: https://arxiv.org/abs/1412.8091 https://arxiv.org/abs/1412.8091 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.