First, let me mention that computers already find new theorems and proofs. In the past years a lot of progress was made in the area of research involving automated theorem provers and proof verifiers (the system Coq, http://coq.inria.fr/, is perhaps the most important one).
Even before this very powerful system a computer program was set up, was fed the axioms of Euclidean geometry, and started spitting out theorem after theorem, with complete derivations. Some of these proofs were new proofs (or forgotten proofs) to well known theorems. Some of the theorems were undoubtedly new, but it is questionable what their worth or interest was.
One needs to understand that doing mathematics does not involve randomly proving new statements that follow from the axioms of any particular system. Nor does a mathematician wake up in the morning, chooses a random set of new axioms, calls the resulting structure BS, and starts proving stuff about such BS's. Such a thing will rightfully be called "BS theory".
Computers are already far better than humans at both of these useless activities. However, when doing mathematics there is some aim in mind. A goal that justifies the particular symbolic manipulations, rendering them far from arbitrary. Computers today can aid mathematicians sometimes when developing new theories or in finding new theorems. Computers can certainly help verify, sometimes very complicated, proofs. But there is today still no indication that (at least in the near future) computers will be able to just on their own produce new pieces of interesting and meaningful mathematics.