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.

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.