Type checking is the same as proof verification. It is called the Curry-Howard correspondence