What are some theorems that currently only have computer-assisted proofs? For example, there's the four colour theorem.
I am very curious about this and would like to generate a list.
Hales' proof of Kepler's conjecture that cubic close packing is optimal uses computer checking of numerous cases.
The proof by C.W.H. Lam et al that there is no finite projective plane of order $10$.
Don't know if if this counts, but the proof that God's number (the maximum number of moves required to solve any Rubik's cube) is 20 is computer-assisted. It involves using an algorithm to solve every possible state of the Rubik's cube along to establish the upper bound of 20 along with a mathematical proof that one specific configuration, the Superflip, requires 20 moves (lower bound).
Here's a very easily understandable one Sudoku fanatics have long claimed that the smallest number of starting clues a puzzle can contain is 17. Now a year-long calculation proves there are no 16-clue puzzles. The Minimum Sudoku problem was tacked by a computer proof by Gary McGuire , Bastian Tugemann , Gilles Civario Here's the paper of their algorithm .
The program that found the proof was a general-purpose automated reasoning program that was only given the Robbins axioms and the negation of a condition $C$ such that $Robbins, C \vdash Boole$ has a simple proof, from which it derived a contradiction.
This makes the proof a bit different from the others here: while the other proofs are like buildings that could only be built using elephants and horses, this is a building built by an elephant. While the first buildings will look like ordinary buildings, only bigger, this one looks quite unfamiliar
Some processor designs are verified using automated theorem verification (such as ACL2 or in-house software). It's nothing romantic like the 4 color theorem, but the "theorems" are huge and practically impossible to verify by hand.
Here's one you're less likely to have come across. It answers the question of how many different slopes on the boundary of a hyperbolic 3-manifold can be exceptional (that is, Dehn filling at that slope gives a manifold that is not hyperbolic). As I understand it, the proof involved checking an upper bound on a continuous quantity (length), and it became important to know the size of the error that could be introduced by the computer.
Four Color Map Theorem.
From more recent and accepted proof by Robertson Sanders Seymour Thomas, JCTB 1997:
The four-colour theorem, that every loopless planar graph admits a vertex-colouring with at most four different colours, was proved in 1976 by Appel and Haken, using a computer. Here we give another proof, still using a computer, but simpler than Appel and Haken's in several respects.
We should mention that both our programs use only integer arithmetic, and so we need not be concerned with round-off errors and similar dangers of floating point arithmetic. However, an argument can be made that our `proof' is not a proof in the traditional sense, because it contains steps that can never be verified by humans.
The evaluation of the Ramsey number R(4,5)=25 by Brendan D. McKay and Stanisław P. Radziszkowski. In human language: the complete graph on $25$ vertices is the smallest complete graph with the property that, if each edge is colored blue or red, there will either be a complete subgraph on $4$ vertices whose edges are all blue, or else there will be a complete subgraph on $5$ vertices whose edges are all red.
Since other answers refer to games (are these really theorems of mathematics?), how about Checkers is solved, Science 2007.
Jonathan Schaeffer and his team at the University of Alberta, Canada, have been working on their program, called Chinook, since 1989, running calculations on as many as 200 computers simultaneously. Schaeffer has now announced that they have solved the game of American checkers, which is played on an 8 by 8 board and is also known as English draughts.
The team directed Chinook so it didn't have to go through every one of the 500 billion billion (5 * 1020) possible moves. Not all losing plays needed to be analysed; instead, for each game position, Chinook needed to work out only a move that would allow it to win. In the end, only 1/5,000,000 of the moves were computed.
As Chinook has worked out all relevant lines of play, it needs virtually no time to 'think' to work out each perfect move in a game.
Checkmate for checkers, Nature 2007.
Consider the sequence board games of perfect information of increasing complexity: Tic Tac Toe < Checkers < Chess < Go (Wei Chi). Tic Tac Toe was already solved by Babbage. Checkers is solved, but chess only heuristically (eg Deep Rybka). The Go game tree is so large that it's a current frontier where tree pruning is abandoned in favor of Monte Carlo approaches.
Adding one more Erd˝os discrepancy conjecture puzzle. Here's an interesting video describing it with links to the paper in the comments https://www.youtube.com/watch?v=pFHsrCNtJu4