Over a decade ago, Georges Gonthier, gave a formal proof of the four color theorem. I have a mental picture of how the proof works, and I'd like to see if it is correct.
The original proof of the four color theorem worked by proving that the four color theorem reduces to a large-but-finite set of graphs all satisfying some easy to check property. Then Appel and Haken wrote a computer program to check all those cases. This was very controversial at the time, especially since it wasn't clear that the program didn't have a bug.
How does the formal proof in Coq go about proving this?
The picture I have in my mind (which may have come from reading about the proof over a decade ago before I knew dependent type theory) was that it worked as follows:
- Write a function, say,
check_graphsin Coq for checking all the finite number of graphs one needs to check to know the four color theorem is true. If this function runs to completion, and outputs, say,
truethen it has checked all the graphs and they all satisfy the desired property.
- Run (or reduce) the function
check_graphsin the Coq kernel to prove the judgmental equality
check_graphs = true. (I vaguely recall hearing that Coq's kernel had to be optimized to handle a computation of this size.)
- Write a tactic proof in Coq of
<statement of four color theorem> <-> (check_graphs = true).
- Put it all together to get a proof of
<statement of the four color theorem>.
Is this basically correct or am I mistaken on how the proof goes? In particular, I'm unsure of my assumption that the main computational part of the proof was done via judgmental equality, rather than via, say, a tactic.