Toward a Language Theoretic Proof of the Four Color Theorem
By Bobbe J. Cooper, Eric Rowland, and Doron Zeilberger
.pdf
[Appeared in Advances in Applied Mathematics 48(2012), 414431.]
Written: June 7, 2010.
While I certainly hope that there does not exist a purely human,
machinefree, 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 BarNatan, in terms of Lie algebras. An equally nice one
is due to Lou Kauffman, in terms of the "crossproduct" 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,
contextfree 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, 616.
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