Toward a Language Theoretic Proof of the Four Color Theorem

By Bobbe J. Cooper, Eric Rowland, and Doron Zeilberger

[Appeared in Advances in Applied Mathematics 48(2012), 414-431.]
Written: June 7, 2010.
While I certainly hope that there does not exist a purely human, machine-free, proof of the Four Color Theorem (if there is, it would mean that this theorem is, a posteriori, trivial!), it is still fun to try and look at more elegant machine proofs. 4CT has quite a few equivalent formulations. A very nice one is due to Dror Bar-Natan, in terms of Lie algebras. An equally nice one is due to Lou Kauffman, in terms of the "cross-product" and the basis vectors i,j,k, we all know and "love" from way back when we took multivariable calculus. But that is just a red herring. An equivalent formulation is in terms of a certain, very simple, context-free grammar, and the 4CT turns out to be equivalent to an elegant simply stated linguistic fact, namely that the CFG
0 -> 12, 0->21, 1->02, 1->20, 2->01, 2->10
is totally ambiguous. In the present article, Bobbe Cooper, Eric Rowland, and I prove, humanly, this statement for many families of pairs of binary trees (alas, not for all possible pairs).

Added May 22, 2014: We just found out from Robert Cori, that the connection between graph colorings and formal language was already discovered in an article in 1986: R. Cori and S. Dulucq, "Colouring of Planar Maps and the Equality of Two Languages", Proc. of CAAP '86, Lecture Notes in Computer Science, v. 214, 1986, 6-16. Here it is .

So this is a natural idea!

Mathematica Package

This article is also accompanied by Mathematica package ParseWords, written by Eric Rowland, available from

Maple Package

This article is accompanied by Maple package

Sample input and output for LOU

  • If you want to prove Lou Kauffman's version of 4CT for n ≤ 8, the input yields the output .

Doron Zeilberger's List of Papers

Doron Zeilberger's Home Page