Where and how did computers help prove a theorem? The purposes of this question is to collect examples from theoretical computer science where the systematic use of computers was helpful


in building a conjecture that lead to a theorem,
falsifying a conjecture or proof approach,
constructing/verifying (parts of) a proof.


If you have a specific example, please describe how it was done. Perhaps this will help others use computers more effectively in their daily research (which still seems to be a fairly uncommon practice in TCS as of today).

(Flagged as community wiki, since there is no single "correct" answer.)
A very well-known example is the Four Color Theorem, originally proven by exhaustive checking.