It seems to me like many of the most famous "computer proofs" were done by basically brute-forcing through all of the cases, such as the four color map theorem. Are there any good examples of computer proofs that did not use this strategy? What strategy did they use?
EDIT: I suppose there have been many proofs by example/counterexample too. I would probably not qualify these as "interesting" unless there's another reason to do so.