18
$\begingroup$

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?

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

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ Some completely superficial and nonconclusive points: Cahit is a genuine mathematician. His work on equitable labelings emu.edu.tr/~cahit/CORDIAL.htm , some of which I have read, is quite mainstream and readable. He has also been claiming for the last 5 years to have a new proof of the 4-color theorem. This work has not appeared in any peer reviewed journal. (continued) $\endgroup$
    – David E Speyer
    Commented Nov 3, 2010 at 13:43
  • 2
    $\begingroup$ If you look at his preprints en.scientificcommons.org/i_cahit , you will see that he often says he has a proof, but often describes his work as an outline or a sketch, or resorts to drawing pictures, rather than focusing on giving a rigorous start-to-end proof. I tried to read his first preprint when it came out, and was unable to understand it well enough to determine whether or not it gives a well-defined algorithm, but I will freely admit that I only worked on it for a single afternoon. (continued) $\endgroup$
    – David E Speyer
    Commented Nov 3, 2010 at 13:43
  • 3
    $\begingroup$ Obviously, the only way to be certain whether or not there is a proof here is for several graph theorists to really sit down and pick these papers apart. (And perhaps some have already done so, and will report in here.) Based on the superficial evidence, there is good reason to be skeptical. $\endgroup$
    – David E Speyer
    Commented Nov 3, 2010 at 13:45
  • 2
    $\begingroup$ So the question reduces to "is Cahit's claimed proof correct?". Questions of this kind often result in unresolvable disagreement: I vote to close. $\endgroup$
    – Robin Chapman
    Commented Nov 3, 2010 at 13:45
  • 5
    $\begingroup$ Robin -- no, the question does not reduce to that: there are other potential approaches, e.g. arxiv.org/abs/q-alg/9606016 and there may be more that I'm not aware of. I for one would be interested to know what these approaches are and what progress if any has been made in that direction. $\endgroup$
    – algori
    Commented Nov 3, 2010 at 13:55

1 Answer 1

Reset to default
30
$\begingroup$

This is too long for a comment, so I am placing it here.

In this article of the Notices of the AMS, Gonthier describes a full formal proof of the four-color theorem, which makes explicit every logical step of the proof.

Although this formal proof has been checked by the Coq proof system, it would seem to be a category error to view this proof as a computer-based proof of the same kind as Appel and Haken's. The situation with Gonthier's proof is that we essentially have a full written text constituting a verified formal proof of the four-color theorem in first order logic.

And that is a state of certainty that most theorems in mathematics, including many of the classical results, have not yet attained.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Oops, that was my comment, forgot to log Andrew out. In Logic I first semester we had to show that solving the four-color theorem was equivalent to showing that the four-color theorem holds for all finite subgraphs, like the Compactness Theorem. But, I didn't solve it all the way. We had to convert everything to the language of colored planar graphs. What is the universe of that structure? $\endgroup$
    – user10290
    Commented Nov 3, 2010 at 14:48
  • 1
    $\begingroup$ The four-color theorem for infinite graphs reduces to finite graphs by the Compactness theorem, since you can write down the theory of what it means to have a coloring (view it as an assignment of the vertices to one of four predicates, subject to the adjacency requirement). If all finite subgraphs are 4-colorable, then this theory is finitely consistent, hence consistent, so there is a 4-coloring of the whole graph. For countable graphs, one can also view this as an instance of Konig's theorem, since the tree of finite partial colorings is finitely branching. $\endgroup$
    – Joel David Hamkins
    Commented Nov 3, 2010 at 15:16
  • 11
    $\begingroup$ Gonthier's proof is still not human-checkable in the usual sense of the term. There's still a lot of case-by-case checking, e.g. of the critical set of 633 reducible configurations. In principle all this computation could be done without machine assistance, but in principle the RSST proof is human-checkable too. The question was specifically about human-checkability and not certainty. $\endgroup$
    – Timothy Chow
    Commented Nov 3, 2010 at 17:50
  • 4
    $\begingroup$ Timothy, I agree with that. My point was merely that there is an enormous difference between using a computer as a computational aide and having a verified formal proof of the statement. For example, these formal proofs can be formally translated to other proof formats to be (re)checked by other totally different proof checkers. After all, formal proofs even of comparatively trivial statements are also very large. $\endgroup$
    – Joel David Hamkins
    Commented Nov 3, 2010 at 18:40
  • $\begingroup$ They can be transformed, and I would love to do that, but that is still a lot of work, since one has to understand both formal systems and then either translate all arguments by hand or built a script to help. $\endgroup$
    – SK19
    Commented May 8, 2018 at 16:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .