Computer Assisted proofs apart from the 4 color theorem I recently read about the 4 color theorem and that it was proved using help from computers. Does anybody know of some other 'good' computer-assisted proofs apart from the 4 color theorem? 
 A: The proof of Kepler's Conjecture by Tom Hales.
It is interesting because the initial informal mathematical proof with the help of some computer programs was considered "99% correct" by some journal reviewers after a few years of banging their head with it, which then motivated Hales to start a project to get it all computer-verified: proper formal machine-checked proofs.  See the Flyspeck Project
A: The arguably second most famous computer proof in Mathematics is the one by Clement Lam showing that there is no projective plane of order 10. The computer part was a huge case-by-case analysis disproving the existence of a certain self-orthogonal code.
A: The proof of The Robbins Conjecture. I find this interesting because the proof was not the computer checking thousands of cases, it was the computer coming up with a relatively simple algebraic proof. My understanding is that the problem was so removed from human intuition and so syntactic in nature that a computer was better able to find a solution just by cleverly searching the space of proofs.
You can see a version of the proof here written up by Allen Mann.
