Fermat's last theorem: How to (partially) solve by programs
See for example Sophie Germain. 
Sophie Germain proved that every prime number p with certain properties could be used as an expoonent in Fermat's Last Theorem.  She used her theorem to prove that all primes up to 100 would work. Apparently checking her theorem was quite a lot of work because later her theorem was used to check first the primes up to 187 and then up to about 1700. Having a computer and being able to check primes using software would have been very helpful. The "intelligent" work was done by Sophie Germain, a lot more boring work could have very well done by a (then non-existing computer). 

Kummer proved an improved theorem, which unfortunately was even harder to verify. There were further improvements made, and this was used to check all primes up to 125,000 and later up to 4,000,000. Checking one prime took about 80 minutes on a 1970's computer - that would have been absolutely impossible to do by hand. 

So there is a combination: Mathematicians find a way to decide for certain primes p that $a^p + b^p \neq c^p$ for all $a, b, c \geq 1$. The actual method to decide is too much work for a human to do in any reasonable time, so a computer comes very useful. 

Wiles' theorem was completely different, all done by hand. However, if you follow the discussion at Wikipedia, you'll find there was mathematics beyond the reach of most mortals, based on more mathematics beyond the reach of most mortals, etc. quite a few levels deep.