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.
This is more of a meta answer in that it is a list of lists.
The papers of Doron Zeilberger. He is a mathematician and his computer is listed at the coauthor Shalosh B. Ekhad on all papers where the computer played a part in deriving the results.
Work of Georges Gonthier. He engineered a machine-checked proof of the four colour theorem and has been recently been working on the Feit-Thompson theorem. He recently completed the formalisation of the Odd-Order Theorem.
Archive of Formal Proofs contains proofs checked with Isabelle, and includes correctness theorems for algorithms, the Gauss-Jordan theorem, some order theory, category theory, and many more classical results.
Formalizing 100 Theorems, contains machine checked proofs of some famous theorems.
One example is the proof of non-existence of a projective plane of order 10.
See The Search for a Finite Projective Plane of Order 10 and The Non-existence of Finite Projective Planes of Order 10.
