Proofs found by computer In 1996, a long-standing open problem was solved by a computer; namely, that Robbins algebra and Boolean algebra are the same. The proof was found by an automated theorem prover.

Moreover, the known proof of Four color theorem contains computer-generated components.

The aim of this question is to list proofs that are (completely or partially) found by computer (whether the only known proof or the one discovered for the first time).
Another famous example is Hales' proof of Kepler's conjecture which had a very large computer aided component.

From Wikipedia:


  In August 1998 Hales announced that the proof was complete. At that stage it consisted of 250 pages of notes and 3 gigabytes of computer programs, data and results.