The claim that dependently typed languages are inherently reliant on fully written-out proof objects looks quite wrong to me. You could easily imagine a proof term with opaque typed "holes" (written `_`) where the content of each "hole" is simply replaced by a LCF-like proof script that was somehow proven (in entirely unspecified ways, having to do with the peculiar programming language that the LCF-like checker uses for its implementation - so the soundness boundary has been expanded a lot, we have given up on having an easily checkable 'kernel'!) to generate some term of the correct type, starting from its environment. Since the content is opaque, no other part of the proof development can tell what exactly was in the hole, and we can dispense with writing that part of the proof term out.

That's how F* (FStar) works, right? You may write out proof objects manually but most of time they are inferred by SMT

That doesn't sound that easy.