Mark Ronan wrote a popular book Symmetry and the Monster (ISBN 0192807234) about the story behind the classification of finite simple groups, or as Ronan calls such groups, the atoms of symmetry. All finite groups can be built up from simple groups somewhat like the way composite numbers are built up from prime numbers. Groups describe symmetries, and so the fundamental building blocks of groups are reasonably called atoms of symmetry. Ronan gave a lecture summarizing his book. Audio, video, and a transcript of his talk are all available here.
The classification of finite simple groups can be seen as a theorem whose proof is spread out over hundreds of articles and thousands of pages. A precise statement of the classification theorem is available here. One major piece of the puzzle is the theorem of Feit and Thompson. An entire journal issue was devoted to the 255-page proof of this one result. There is a project to simplify the proof, eliminating some of the redundancy between papers, etc. But it appears that the revised proof will still contain hundreds of pages of highly technical reasoning.
I enjoyed reading Ronan’s book a couple weeks ago. The biographical sketches in the book are the best part. The book begins with the study of symmetry via group theory, starting with the work of Évariste Galois and Sophus Lie. Someone with very little background in math could read most of the book. However, toward the end of the book when Ronan gets to the classification theorem and the role of “the monster,” he goes into more detail and there I believe he loses his audience. He goes into more detail than a non-mathematician would want to read, but not enough detail for a mathematician to understand exactly what he’s talking about.
I recommend starting with Mark Ronan’s lecture. If you want to go further, read the book, but feel free to skim over details toward the end.
(I haven’t seen a definitive count of the number of journal pages that comprise the classification proof. Ronan quotes one source who says the number of pages is “at least 3,000.” Other sources say “tens of thousands of pages.” Maybe it is unclear which papers should be included.)
i had the same feeling:
by the end, i’m thinking
“who is this written *for*?”.
very cool book, though.
I’ve just read the book, and liked it. Though an unfortunate side effect is I’m now less convinced that all the finite symmetry groups have been found, than I was before I started. The way Ronan tells it, makes me feel like a group could have been missed somewhere in the gargantuan proofs.
I’d be curious how many lines of code in a theorem prover like Coq it would comprise.
I wish I’d heard about this book sooner. Sounds like a good intro (at least up to the end) of the math that software patterns people should understand better, in order to understand more about symmetry and symmetry breaking.
Meanwhile the Feit Thomson theorem has been checked from first principles by George Gonthier and a group of collaborators (using coq) see http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ or the actual article https://hal.inria.fr/hal-00816699/file/main.pdf