How does the formal proof of the four color theorem work?

Question

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_graphs in 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, true then it has checked all the graphs and they all satisfy the desired property.
• Run (or reduce) the function check_graphs in 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.

Answer 1

If you look at section 4 of the extended version of his paper, Gonthier explains how the computation is handled in his proof with the function check_reducible and the theorem check_reducible_valid.

Answer 2

Lolo pointed me to the right reference (A computer-checked proof of the Four Colour Theorem) and even the exact page numbers to look at (pp 11, 12). However, I want to provide a more stack exchange compatible answer for others who reach this.

It was already known that to prove the Four Color Theorem, it was enough to check that a particular list of 633 "configurations" are all "reducible". It doesn't matter here exactly what this means except that

• A configuration is a finite object that can be written as something like Config 11 33 37 H 2 H 13 Y 5 H 10 H 1 H 1 Y 3 H 11 Y 4 H 9 H 1 Y 3 H 9 Y 6 Y 1 Y 1 Y 3 Y 1 Y Y 1 Y in Coq.
• Checking that a configuration is reducible is a computation.
• I assume that that somewhere in Coq is a proof that if all of these 633 configurations are reducible, then the FCT holds.

So now all one has to do is check that all 633 configurations are reducible. To do this, the paper describes two definitions in Coq:

Variable cf : config.
Definition check_reducible : bool := …
Definition cfreducible : Prop := … 

So because of the variable, check_reducible is a term of type config -> bool and should be thought of as a computer program checking that a configuration is reducible. On the other hand, cfreducible is a term of type config -> Prop, which gives a mathematical definition of reducibility.

Then they have a lemma (also under the variable)

Lemma check_reducible_valid : check_reducible -> cfreducible.

This states (because of conversion from bool to Prop) that if check_reducible cf = true then cfreducible cf. In other words, it shows that the program check_reducible really does check that a configuration is reducible.

Finally, the document suggests that they had a bunch of lemmas of the form

Lemma cfred232 : (cfreducible (Config 11 33 37
 H 2 H 13 Y 5 H 10 H 1 H 1 Y 3 H 11 Y 4 H
 9 H 1 Y 3 H 9 Y 6 Y 1 Y 1 Y 3 Y 1 Y Y 1 Y)).

One for all 633 configurations. The paper suggests that this lemma was proved via two steps: apply check check_reducible_is_valid and prove true = true by computing check_reducible. So I assume something like

Proof.
  Apply check_reducible_is_valid.
  Reflexivity.
Qed.

But this isn't made clear. At the time it took them an hour to check this one lemma.

---

Looking at the current version of the project which palmskog posted, it seems that they now batch configurations in groups, and have lemmas like red00to106:

Lemma red000to106 : reducible_in_range 0 106 the_configs.
Proof. CheckReducible. Qed.

The LTac code for CheckReducible is here, but I'm not certain what it does. The final four color theorem proof is here.