# What about dependent types is useful for theorem provers?

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?

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).