There are two things at play here. The first is about having different kernels for basically the same proof assistant. That is, having different programs that are all able to type-check essentially the same proofs. This is something the Lean community is quite keen on, for instance, with various external kernels implemented in various languages. But it seems this is not what you are after.
Instead, as far as I understand, you would like to be able to somehow communicate proofs between different proof assistants/kernels. The difficulty, here, is that basically all proof assistants have different logics. Some are relatively close (Rocq and Lean, for instance, are so close that at some point there was an exporter from the latter to the former), some are much further apart (for instance, Isabelle's HOL foundation is quite different from the dependent type systems used in Agda, Rocq, Lean…). The issue with this is twofold.
The first issue is called concept alignment. The issue is that, to be able to transfer a theorem between systems, you need to be able to translate its statement from one logical formalism into the other. This can seem like a trivial task, and indeed if the statement is e.g. about natural numbers, the translation can be relatively direct. However, for more complex/interesting statements about more complex/interesting objects, this would not be as easy at all! Think, for instance, about a statement about algebraic closures, or vector fields, or… And this is compounded by the fact that even in relatively close logical formalisms, choice can differ wildly in the way you set up definitions. Yet, you'd really like to make sure that you did not make a wrong statement about a subtly different object.
Second, while translating one single theorem might be vaguely useful, more often than not you would like to transfer an entire library, say a series of result about algebraic closures, rather than a single one. This makes concept alignment even harder, and especially so since different systems have different approaches to organising libraries. And typically libraries do not consist only of definitions/theorems, there are also all other sorts of objects, for instance including tactics/tactic scripts. Being able to make these communicate is even harder!
I do not wish to mean that translating between proof assistants is unfeasible, and multiple projects, in particular Dedukti which you mentioned, are trying hard to see what is feasible in this space. But at the moment at least it remains a long-term research question to achieve this sort of communication.
