Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?"

share|improve this question

closed as not constructive by Austin Mohr, LVK, copper.hat, wentaway, Quixotic Sep 4 '12 at 12:33

As it currently stands, this question is not a good fit for our Q&A format. We expect answers to be supported by facts, references, or expertise, but this question will likely solicit debate, arguments, polling, or extended discussion. If you feel that this question can be improved and possibly reopened, visit the help center for guidance.If this question can be reworded to fit the rules in the help center, please edit the question.

I would disagree with your characterization of a proof that proceeds by checking a large number of cases. In a sense, the Appel-Hanken proof relies on a structure theorem by showing that every graph must contain one of the reducible subgraphs; it's just that there are many such subgraphs. –  Arturo Magidin Jan 13 '12 at 4:20
@Arturo Magidin Right. That is a better way of looking at it. I guess what I'm asking, for this specific case, is if we can put a bound on the number of those graphs? Or perhaps a theorem telling us why there are so many? Perhaps I should revise my question. –  Harry Stern Jan 13 '12 at 4:26
@ArturoMagidin also thank you for fixing the tags; I wasn't really sure what to do with them. –  Harry Stern Jan 13 '12 at 4:36
The CFSG is a very elegant proof by cases: there are only 3 kinds of finite groups without normal subgroups of odd order or even index: (1) No elementary abelian subgroups of rank 3, (2) A centralizer of an involution looks like the centralizer of an involution in a matrix group in odd characteristic, (3) A centralizer of an involution looks like the centralizer of an involution in even characteristic. That these 3 cases are exhaustive is at least somewhat surprising but almost textbook level, and indicates a way in which most simple groups are of Lie type. The sub-cases are interesting too. –  Jack Schmidt Jan 13 '12 at 6:08
In other words, if we didn't solve it by cases, then we would lose something: the fact that fusion-simple groups divide up nicely into these nice cases. The rest of the proof is just being more specific about what groups in those cases look like. –  Jack Schmidt Jan 13 '12 at 6:10