Different systems can have very different logical foundations, so converting proofs from a system to another can be very complicated in general. Even when conve

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/ 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 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.