> Automated theorem checking is typically very difficult for any nontrivial theorem

I'm not sure this is true -- I thought the whole idea of these theorem systems was to make the kernel of the proof system as simple as possible (to allow a manual proof, or at least high confidence of correctness).

If your program can produce an instance of a type, and it type-checks, then it true. Type inference can be tricky, and a lot of what makes the systems usable is the fact that you can omit types and allow the compiler to infer them, but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof.