Different systems can have very different logical foundations, so converting proofs from a system to another can be very complicated in general. Even when converting is possible, the converted proof might be very anti-idiomatic in the target system, in more or less the same way one automatically converting Haskell to C is likely to produce very anti-idiomatic C. Also, communities do not necessarily compete for this list.

Keeping this in mind, there still is something:

* OpenTheory (http://www.gilith.com/opentheory/) provides some kind of lingua franca between systems of the HOL family, that are rather similar.

* Mario Carneiro wrote an article (https://arxiv.org/abs/1412.8091) on automatic conversion from OpenTheory to Metamath. I am not aware of an actual implementation.

* Although it is not the same things, some systems have tools that can feed a subproof to an ATP (automated theorem proved) and reconstruct a valid proof to it. That simplifies proof writing.

I did not a comprehensive review, so the list may be lacking.

The ones I'm familiar with avoid Turing-completeness in order to ensure that all functions are total. In doing so, they remain quite expressive but not enough to write interpreters for themselves. So the usually straightforward strategy of embedding a language by writing an AST datatype and interpreter is unlikely to work in this space.