What are some theorems that currently only have computer-assisted proofs?

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.

Solution 1:

Hales' proof of Kepler's conjecture that cubic close packing is optimal uses computer checking of numerous cases.

Solution 2:

The proof by C.W.H. Lam et al that there is no finite projective plane of order $10$.

Solution 3:

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).

Solution 4:

Tucker's proof of the existence of a chaotic strange attractor in the Lorenz equations.

For a list of other theorems proved using interval methods, see Proving Conjectures by Use of Interval Arithmetic by Andreas Frommer.

Solution 5:

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 .