I don't know if there exist computer programs working on its own, trying to find and prove theorems, delivering proofs and go on searching for new theorems. But if (when) there are such programs, efficient or not, would it be a milestone in the development of mathematics? Or would lack of intuition and heuristic create nothing more than lists of random theorems, not much more important than lists of random numbers?
Isn't mathematics more than pseudo random started recursive processes? How important is human desire for the development of important and realistic mathematics?
The fact that such a program exists is actually an important concept, in fields such as foundations of mathematics, computability theory and complexity theory.
Foundations: When you want to reason about mathematics in general, you can either fix an axiomatic system, such as ZF (or a variant like ZFC), or take a general one. However, when you consider a general axiomatic system, you usually require that this system is recursively enumerable, which means precisely that there exists a program that enumerates all proofs and theorems in your given system. This is for instance required in Gödel's incompleteness theorems. In particular it is true in the case of ZF(C), which is the system most commonly used by mathematicians.
Computability: When studying Turing machines, you might be interested in proving termination. The fact that there is a particular Turing machine that enumerates proofs in your system (like ZFC) shows that you will not be able to always find a proof that tells you if your algorithm terminates. For instance if you take an machine that looks for a contradiction in ZFC, and if ZFC is coherent, your machine won't terminate but you cannot prove it in ZFC (as showed by Gödel in his second incompleteness theorem). So the fact that your system is recursively enumerable implies a limit on what you can prove about Turing Machines: there is a particular explicit Turing Machine that runs forever but you cannot prove that fact.
Complexity: Finally, it is argued that the question of P=NP is linked with automated proving. Indeed, looking for a proof is a priori a lot harder than checking the validity of a proof. But if P=NP, verifying becomes "as hard" as finding, and so it would become "easy" to find proofs automatically, when they exist and are not too long. However, even if P=NP, the algorithm could still be impractical because of huge constant or exponent, but in spirit mathematicians could be replaced by algorithms.