1. Yes, but the situation regarding type inference is only a bit worse than the situation in non-dependently-typed languages. Of course the compiler can't magically figure out what theorems you want to prove.
This is my point. Adding dependent types comes with costs that you will always have to pay, even if you don't use the power of dependent types. If you verify with e.g. program logic in the few real-world cases where formal verification is financially viable, then you only pay the price when you do the verification.