By Bobbe J. Cooper, Eric Rowland, and Doron Zeilberger
So this is a natural idea!
.pdf
[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 .
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
Doron Zeilberger's List of Papers