I got to talk with George Gonthier at the DIAMANT symposium last week. One thing I learned about his proof is that he uses hypermaps more extensively than I had thought. What he actually shows is that every planar hypermap is four colourable.
Every graph has an associated hypermap, but hypermaps are more general. In particular edges in hypermaps can be adjacent to more than two faces. In fact, hypermaps are completely symmetric in terms of vertices, edges, and faces. I’m not entirely sure how to picture planar hypermaps, but there is a corresponding Euler formula to tell you when a hypermap is planar.
The first step in proving the four colour theorem is to reduce the problem to one where every vertex is of degree three. My understanding is that when you do this with hypermaps, the edges are also reduced to having two faces, so this extension of the four colour theorem isn’t such a big deal. None the less, Gonthier uses these more general maps in an essential way in his proof; this tool was not available in the original proof of the four colour theorem. It is analogous to using the complex numbers to prove properties of the real numbers. I wonder if graph theory is missing out.
I also heard of a way of representing algebraic real numbers. It is clear that you want to use an integer irreducable polynomial to represent an algebraic number, but the question of how to distinguish between the different roots remains. The traditional answer seems to be to put little boxes around each root to isolate them from each other, but this brings in analysis to solve an algebraic problem, which isn’t very pleasing. Apparently the answer is to use the sequence of signs of the derivatives of the irreducible polynomial at each root to distinguish between them. I’d be interested to know more about operating on the algebraic numbers this way.