Hm... I'm not so sure about that. Of course, if we're speaking about dependent types, then yes. However, theorem proving could also be done automatically, by an

Hm... I'm not so sure about that. Of course, if we're speaking about dependent types, then yes. However, theorem proving could also be done automatically, by an external theorem prover, which would only need the refined type annotations on your variables to prove stuff (using the whatever theories the theorem prover knows about, such as linear integer mathematics, logic, real nonlinear math, vectors, datatypes, etc).