The form of the classification theorem that I had heard before was like:

A group G is an "abstract reflection group" iff there exists an n and some numbers m_ij for i and j ranging over 1..n such that G is (isomorphic to) the group generated by n generators c_1...c_n, subject to equations c_i^2 = 1, and (c_i c_j)^(m_ij) = 1. All of the abstract reflection groups that *happen to be finite* correspond exactly to coxeter-dynkin diagrams. Here's how to find the group, given the diagram: The number n is number of vertices in the diagram. The m_ij are gotten by looking at the edge (if any) between vertex i and vertex j. If there is no edge, m_ij is 2. If there is an unlabeled edge, m_ij is 3. If there is an edge with a number on it, m_ij is that number.

The trouble with trying to play with this problem naively --- to see how one might discover the classification from scratch, or even verify parts of it --- is that reasoning about equality of group elements, and therefore understanding whether a presented group is finite, is really hard! Undecidable, in fact.

So the thing that excited me about the proof in the Big Tome above is that it gave a nice, easy-to-compute necessary and sufficient condition on a bundle of numbers m_ij that tells you whether the reflection group is finite. All you have to do is check whether the matrix -cos(π/m_ij) is positive definite, which reduces by Sylvester's Criterion to just computing a whole bunch of determinants. Why this condition is necessary and sufficient is still pretty mysterious, but I'm starting to almost understand it in terms of the little chunks that a concrete reflection group in (n+1)-dimensional euclidean space carves up the n-sphere into.

Anyway it's really comforting to see the calculation of the determinant of the cosine matrix for A_4, D_5, E_6, E_7, E_8 go like 5, 4, 3, 2, 1... which then "explains" why there's no E_9. It ran out of determinant!