# 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
As I know, proof of the 4ct has only around some thousands of cases. It seems to me human checkable, although probably not the best usage of his time for a mathematician. – peterh Jan 18 at 23:10
@peterh: It depends on how much time it takes to check each case. The 4CT was proved by finding a set of unavoidable configurations, that is, a set with the property that every planar map contains at least one of the configurations in the set, and then showing that every member of this set is reducible. Each unavoidable configuration consisted of a ring of countries with at least one country in the interior of the ring. Reducible means that there is a way of extending any four-coloring of the ring and its exterior (which is arbitrary) to the interior. – Will Orrick Mar 17 at 13:32