There are a good number of theorem provers which use dependent typing as a part of their type systems. It seems this proportion is much higher than in programming languages.
So what is useful about dependent types for theorem provers specifically? What design problems do they solve?
A general-purpose proof assistant must be built on a foundation that is strong enough to represent most or all of mathematics, since proofs take place in mathematics. Dependent type theory, like higher-order logic and set theory, fits this bill, while non-dependent type theory does not.
(Your question suggests you're asking about the suitability of dependent type theory versus non-dependent type theory for a proof assistant. Preferences between dependent type theory and higher-order logic or set theory are more opinion-based.)
The essential point is that you have to be both able to define structures and define and prove predicates about those structures. So you need at least one level of "dependency": predicates depend on structures. Higher-order logic has exactly one level of dependency, while dependent type theory has arbitrary dependency, and set theory allows arbitrary dependency to be encoded in terms of membership.
Dependent types allow quantifiers over values, which is very important in describing propositions. This is impossible in, for example, simple type theory (on the other hand, it is not necessary to represent propositions using types. You may use a separate language for propositions).
For example, $\forall a\in\mathbb N.\forall b\in\mathbb N.a+b=b+a$ is a dependent type (well, this assumes a type-theoretical definition of $=$), which is a dependent function type with two parameters of type $\mathbb N$, that can be applied (just like normal function application). For example, applying an argument $0$ to it results in another dependent function of type $\forall b\in\mathbb N.0+b=b+0$.
Apart from forall quantifiers, mathematical structures such as groups, rings, categories can also be represented by a dependent type (a dependent tuple type). For example, $\exists A\in \mathcal U. a\in A$ represents a pointed set (the symbol $\mathcal U$ contains all small sets).
