Two main difficulties. Incompleteness (see Gödel's Incompleteness Theorems) and the vast size of the search space (there are vastly more uninteresting theorems than interesting ones). Considerable progress has been made using proof assistants (Coq, Isabelle, Agda, etc). With these the mathematician writes the theorems and lemmas and the proof assistant helps finding proofs and ensures that the proofs are logically valid.
One simple way a computer could prove a new theorem is to take two existing theorems, $P$ and $Q$ and combine them to make the theorem $P\wedge Q$. Of course, if the search procedure is more clever, then you can discover more clever things, but to find something truly interesting and original would require a lot of intelligent tricks and techniques on the part of the programmer. Gödel's incompleteness theorems are relevant here because they place a fundamental limit on what can be discovered within any proof system: a computer could never discover the proof of the consistency of its own logic.
This paper describes how the proof assistant Coq is used to prove the four colour theorem. Mechanized mathematics (overview ) is one area of TCS devoted to (semi)automatically proving theorems (and in general using computers to help mathematicians).
One area where automated theorem proving (of sorts) is making an impact is in model checking and model finding. Model checking deals with determining whether a given system satisfies a given property, whereas model finding finds a system to satisfy a given collection of properties. The tool Alloy employs model checking and model finding to good effect, and it's quite usable.