This post over at the n-category cafe has got me thinking about the classification of finite simple groups. As I said in the comments over there, the thing that fascinates me most about the story of classification (aside from the fact that I heart finite groups) is sociologically what went wrong with finite group theory that made the energy from classification dissipate so that very few young researchers keep its ideas and spirit alive.
When I was thinking about this I did some poking around trying to understand a little more about the odd order theorem (which is something I would genuinely like to understand in detail at some point in my life). The wikipedia article on Feit-Thompson is very high quality, and Stephen Harris sent me a link to an expository article by Glauberman. The impression that these articles give is that the outline of the Feit-Thompson argument isn’t too difficult to understand, but that the details get quite annoying and the argument splits into a number of cases. This got me wondering: “maybe the classification theorem could aspire to become more like the four-color theorem?”
Bear with me for a second here, I know that many people hate the computer proof of the four color theorem, and certainly it’d be nice to have a short conceptual proof of it (see Week 22). Nonetheless I think there are a lot of advantages to the four color theorem over parts of the classification theorem. First off, it’s not that hard to understand how the argument goes, there’s some simple nice ideas and then a huge number of cases any one of which is understandable. My impression is that a mathematician who put her mind to it could pretty much understand this proof in at most a couple weeks (the same is not true of the odd order theorem, let alone the full classification). Secondly, the computer proof of the 4-color theorem is quite reliable and much much more likely to be correct and true than the classification theorem. (Some people seem to consider computer proofs as bad because they are unreliable, these people are either lying or crazy. There are lots of issues with computer proofs, but reliability relative to a long computation in a journal article is not one of them.)
So the idea I’m proposing here is that a different way to clarify the classification project (as opposed to shortening the traditional argument, or making a computer verifiable proof) would be to try to reduce it to a collection of algorithmic tests which can eliminate groups satisfying certain properties. You explain each of these algorithms, you then have a computer package which can apply all applicable tests until it kills off a case. In the end you have a computer program that applies these algorithms to a huge set of cases, and in the end spits out a classification of simple groups. Because the arguments that the computer is doing implicitly wouldn’t end up in the final write-up you could hope to get a much shorter human understandable book that together with the computer program would give a proof of classification. I think in this form it would be much easier for people to understand and use the ideas in this project.