The four color theorem's only widely known proof is of course Appel and Haken's computer-assisted one. How likely is it that this the only proof, and might there be some way to prove that this is so?
Wikipedia lists these: The proof that there is no finite projective plane of order 10, the classification of finite simple groups, and the Kepler conjecture as other problems whose only known solutions involve checking lots of cases.
More generally, is there a way to prove that a problem can only be solved by checking a large number of cases? Such a solution would be like an anti-structure theorem, saying that the object does not have sufficient structure for a fact to necessarily be true (but the case analysis shows that it "happens to be so").
It seems like recreational games that have some sort of logical or algorithmic component are another source of these problems. Finding the minimum amount of moves to solve any rubik's cube or solving the minimum sudoku problem are two examples of such games that have been solved fairly recently by computers.
EDIT: I was not specific enough. The main question here is "Is it possible to show that the only proof of a theorem (which otherwise might seem to have a different proof) can only be done via considering a large number of cases?"