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 mathem

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.