The systems you mention use a declarative proof approach that's more similar to the way humans might write a math proof, or to the way computer code is written. In contrast, Coq and Lean use "proof scripts" that are more like writing your stuff in a custom macro-assembler that will break as soon as one changes anything in the "script", or even just upgrades to a newer version of the underlying software. Even the resulting proof is basically not readable on its own without re-processing it with the software itself. (Coq used to have a declarative "mathematical proof language", but it was unmantained and they removed it.)

Other systems, e.g. Agda use "proof terms" that are more like a proof that can be read "declaratively", but one where every single step has to be recorded; there's no provision for the system to "fill in" some gaps, unlike with declarative proofs. This can definitely impact readability/surveyability of a development, but the inherent maintainance problems of "proof scripts" do not arise.

I'm not sure what Dedukti is going for from this basic POV. They mention that they're trying to build a general framework that can support multiple logical/proof systems, but the details are not that clear. It's probably going to be a bit clunkier than the systems you mention, particularly at this early stage of development.

I thought Dedukti has a small kernel. Although “small” may be a relative thing (relative to other dependently typed systems.

You can also add Coq's to the mix:

[3] https://coq.inria.fr/library/

Each 1-3 is language specific (Isabelle/HOL, Mizar and Coq respectively).

Logipedia too, is using the language Dedukti, although it is designed to translate into other proof languages, and list these on Logipedia.