Comment by overfeed

The first major computer-assisted proof, of the four-color map theorem in 1976, was an example of this. It created a lot of controversy at the time. It used proof by exhaustion, i.e. essentially analyzing every possible relevant case, something that no human could do without the assistance of, at the time, a supercomputer.