I'm not an expert on this by any means, but from what I've read about the four-color theorem, essentially all of the insight in the proof came from human mathematicians. Mathematicians figured out an ingenious way to reduce to the problem to carrying out a a large number of tedious computations, and the computer was used only to carry out those computations and thereby complete the proof. This seems quite different from a computer coming up with a proof by itself.