# Human checkable proof of the Four Color Theorem?

Four Color Theorem is equivalent to the statement: "Every cubic planar bridgeless graphs is 3-edge colorable". There is computer assisted proof given by Appel and Haken. Dick Lipton in of his beautiful blogs posed the following open problem:

Are there non-computer based proofs of the Four Color Theorem?

Surprisingly, While I was reading this paper, Anshelevich and Karagiozova, Terminal backup, 3D matching, and covering cubic graphs , the authors state that Cahit proved that "every 2-connected cubic planar graph is edge-3-colorable" which is equivalent to the Four Color Theorem (I. Cahit, Spiral Chains: The Proofs of Tait's and Tutte's Three-Edge-Coloring Conjectures. arXiv preprint, math CO/0507127 v1, July 6, 2005).

Does Cahit's proof resolve the open problem in Lipton's blog by providing non-computer based proof for the Four Color Theorem? Why isn't Cahit's proof widely known and accepted?

Cross posted on cstheory.stackexchange.com as Human checkable proof of the Four Color Theorem?

-
It's on MO, too. – J. M. Nov 3 '10 at 13:27
The question presupposes that Cahit's claimed proof is actually correct. – Robin Chapman Nov 3 '10 at 13:52
I don't understand why is there so much appeal for a human checkable proof of this result? Why aren't people demanding a human checkable proof that 615789648168*54681684648 = 33672415350625446924864? (If you can actually do that yourself then triple the number of digits.., it's just an example to illustrate my question anyway) – anon Nov 3 '10 at 17:03
Muad, I think that what people want most of the time is insightful proof - proof that not only tells us "it's correct" but also helps us understand WHY it is correct. A human-verifiable proof is not, of course, always an insightful proof; but it's a start. – Gadi A Nov 4 '10 at 16:40
To @Gadi's point: "If your solution breaks into cases, then you don't understand the problem." ;) I was given this as a rule of thumb many years ago, but I don't have an attribution. – Blue Nov 4 '10 at 17:21

After reading the papers by Rufus Isaacs [1] and George Spencer-Brown [2], I have reached to the conclusion that spiral chain edge coloring algorithm [3] gives answer to the question in affirmative.

[1] Rufus Isaacs, "Infinite families of nontrivial trivalent graphs which are not tait colorable", American Math Monthly 73 (1975) 221-239.

[2] George Spencer-Brown, "Uncolorable trivalent graphs", Thirteenth European Meeting on Cybernetics and Systems Research, University of Vienna, April 10, 1996.

[3] I. Cahit, Spiral Chains: The Proofs of Tait's and Tutte's Three-Edge-Coloring Conjectures. arXiv preprint, math CO/0507127 v1, July 6, 2005.

-
Link to George Spencer-Brown paper: omath.org.il/image/users/112431/ftp/my_files/… – Cahit Jul 6 '11 at 6:42
Actually Tutte-conjecture asserts that "Every 2-connected cubic graph with no Petersen minor is 3-edge colorable" and extends Tait-conjecture to all 2-connected cubic graphs. Robertson, Seymour and Thomas (RST) conjecture that (1) Every 2-connected apex cubic graph is 3-edge colorable and (2) every 2-connected doublecross cubic graph is 3-edge colorable strengthened Tutte-conjecture that the only possible counter-examples are either apex or doublecross cubic graph. In [3] by using spiral chain edge coloring algorithm we have shown that this is not the case. – Cahit Jul 7 '11 at 9:41

Any proof of the 4CT is human-checkable so long as that human has enough time on their hands.

-
And lives long enough... Which is a significant restriction! Could you check a proof of $10^{15}$ words/symbols if you had enough time on your hands? – Joseph O'Rourke Dec 4 '10 at 17:07
What about mistakes? – SamB Dec 4 '10 at 23:31
@Joseph I am almost sure that "having enough time" implies "having enough time alive". Humm... so medical technology may contribute to the advancement of mathematics! – Willie Wong Jul 6 '11 at 12:01