Is there a reasonable automated proof system for TCS theorems?
Here is an Isabelle/HOL library containing Rice's theorem, which states undecidability of a wide range of problems. Since this library models computability via recursive functions, you have to encode a universal Turing machine as a recursive function in order to use this theorem for proving undecidability of the halting problem of Turing machines.  However, the essential parts of the undecidability proof is already done.

http://afp.sourceforge.net/browser_info/current/HOL/Recursion-Theory-I/index.html