There already have been cases of theorems being proven by computers. I don't know how much truly original work, but I remember (faintly) at least one case where

There already have been cases of theorems being proven by computers. I don't know how much truly original work, but I remember (faintly) at least one case where the computer discovered an unknown way to prove an existing theorem. Many years ago I was on a logic conference and one speaker proposed to make "a computer can solve it automatically" the definition of trivial (as in "this is trivial to solve").