11
$\begingroup$

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.

$\endgroup$
3
  • 2
    $\begingroup$ This is not really a historical question, since the code which builds the Coq proof is available on GitHub and works with Coq version 8.11 or later. It might be better to rephrase as asking how the code currently works. $\endgroup$
    – palmskog
    Mar 19 at 21:50
  • $\begingroup$ @palmskog Just looking through that file, it seems that there is a particular tactic, CheckReducible, that is used to check the individual configurations (in the jobs files in the theories folder), and plays the role of check_graphs in the Jason's picture. $\endgroup$
    – Will Sawin
    Mar 19 at 22:40
  • 1
    $\begingroup$ I wrote an explanation here. $\endgroup$
    – Trebor
    Mar 20 at 1:34

2 Answers 2

8
$\begingroup$

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.

$\endgroup$
2
  • 3
    $\begingroup$ Thank you for the link. I think it would be greatly appreciated if you could give a short summary instead of just taking us to the depths of the actual paper. $\endgroup$ Mar 23 at 14:39
  • 1
    $\begingroup$ I find page 11 and page 12 a pretty good overview of how computation is actually handled, you don't need to read the full paper. It is pretty close (but more precise) to what jason was describing. $\endgroup$
    – Lolo
    Mar 23 at 16:16
8
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ just a little comment, now comfigurations are grouped so to maximize parallel computations. On my laptop it takes 6 minutes (42m if you do it on a single core). The theorem the_reducibility is the one that collects the 633 configurations. The theorem unavoidability is the one that shows that these 633 are unavoidable. $\endgroup$
    – Lolo
    Mar 25 at 12:12
  • 1
    $\begingroup$ A bit of extra: what Gonthier's proof essentially does is to verify the correctness of the hand, computer assisted proof produced by Robertson, Sanders, Seymour, and Thomas. It is useful to understand that work. You can find an expository version of that at the link below, and links to the actual paper: thomas.math.gatech.edu/FC/fourcolor.html $\endgroup$
    – EGME
    Mar 27 at 9:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.