Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

Four Color Theorem (4CT) states that every planar graph is four colorable. There are two proofs given by [Appel,Haken 1976] and [Robertson,Sanders,Seymour,Thomas 1997]. Both these proofs are computer-assisted and quite intimidating.

There are several conjectures in graph theory that imply 4CT. Resolution of these conjectures probably requires a better understanding of the proofs of 4CT. Here is one such conjecture :

Conjecture : Let $G$ be a planar graph, let $C$ be a set of colors and $f : C \rightarrow C$ a fixed-point free involution. Let $L = (L_v : v \in V(G))$ be such that

  • $|L_v| \geq 4$ for all $v \in V$ and
  • if $\alpha \in L_v$ then $f(\alpha) \in L_v$ for all $v \in V$, for all $\alpha \in C$.

Then there exists an $L$-coloring of the graph $G$.

If you know such conjectures implying 4CT, please list them one in each answer. I could not find a comprehensive list of such conjectures.

share|improve this question
4  
"They didn't have a bug in Coq and no cosmic rays flew through their computer when they checked the 4 color theorem" is one such conjecture. –  Andrej Bauer Apr 17 '13 at 10:02
add comment

16 Answers 16

4CT is equivalent to:

share|improve this answer
add comment

Another mechanical verification of the 4-colour theorem has been done by George Gonthier at Microsoft Research Cambridge. The difference with his proof is that the entire theorem has been stated and mechanically verified using the Coq proof assistant, whereas the other proofs contain only the kernel calculation written in Assembly Language and C, and thus have a risk of being buggy. Gonthier's proof covers both the calculational aspects and the logical ones in just 60,000 lines of Coq.

share|improve this answer
add comment

Look at T. Saaty, Thirteen colorful variations on Guthrie's 4-color conjecture, American Math. Monthly, 79 (1972) 2-43 for many examples.

Also, in David Barnette's book Map Coloring, Polyhedra, and the Four-Color Problem, MAA, Dolciani Series, Volume 8, 1983 many examples are given. One particularly interesting result in Barnete's book is: If it is always possible to truncate vertices of a convex polyhedron so as to to produce a 3-valent convex polyhedron so that the number of sides of each face is a multiple of three, it implies the truth of the four color conjecture.

share|improve this answer
add comment

I have talked about this on my blog and our insight is: for example Tait's condition can be weaken to there is a coloring that has at most o(n) errors. See here: http://rjlipton.wordpress.com/2009/04/24/the-four-color-theorem/

share|improve this answer
1  
Really cool! Thanks for this reformulation! –  Hsien-Chih Chang 張顯之 May 10 '11 at 14:47
add comment

In the paper Absolute Planar Retracts and the Four Color Conjecture, Pavol Hell proved several equivalente formulations for the 4CT. One of them reads as follows:

Every planar graph is 4-colorable (The 4CT) iff there exists an absolute planar retract.

(A subgraph $H$ of a graph $G$ is a retract of $G$ if there exists a homomorphism $r: V(G)\to V(H)$ such that $r(v)=v$ for all $v\in V(H)$. An absolute planar retract is a planar graph which is a retract of any planar graph of which it is a subgraph.)

share|improve this answer
add comment

Every bridgeless cubic planar graph is 3-edge-colourable. (This is equivalent to 4CT, due to Tait.)

share|improve this answer
6  
You mean every cubic planar graph, right? –  Ross Churchley Mar 26 '11 at 3:39
add comment

Dror Bar-Natan's paper "Lie Algebras and the Four Color Theorem" (Combinatorica 17-1 (1997) 43-52, last updated October 1999, arXiv:q-alg/9606016) contains an appealing statement about Lie algebras that is equivalent to the Four Color Theorem. The notions appearing in the statement also appear in the theory of finite-type invariants of knots (Vassiliev invariants) and 3-manifolds.

share|improve this answer
add comment

Proposition 2.4 in this paper http://www.sciencedirect.com/science/article/pii/0012365X9500109A# gives another formulation for the 4CT.

Edit: For a given graph $G$, the graph $\Delta(G)$ has the edges of $G$ as its vertices; two edges of $G$ are adjacent in $\Delta(G)$ if they span a triangle in $G$. Then the 4CT can be stated as follows: For every planar graph $G$, the chromatic number of $\Delta(G)$ equals to the clique number of $\Delta(G)$.

I forgot to mention that Albertson and Collins previously proved in the paper
http://www.sciencedirect.com/science/article/pii/0095895684900352 the following similar fact: Given a graph $G$, let $K(G)$ denote the graph whose vertices are the edges of $G$. Two vertices of $K(G)$ are adjacent if the corresponding edges in $G$ are contained in a clique.
Then the 4CT is equivalent to: For any planar graph $G$, the chromatic number and the clique number of $K(G)$ are equal.

share|improve this answer
4  
Can you describe it here, for those of us who don't have access (or like me are too lazy to turn on the VPN to get access)? –  David Eppstein Dec 31 '12 at 5:22
add comment

The high-level description of the automated proof by Gonthier is worth reading, if you are looking for more insight.

Yuri Matiyasevich studied several probabilistic restatements of the Four Colour Theorem, involving positive correlations between two notions of similarity between colourings. His proofs of equivalence rely on an associated graph polynomial, which provides another likely pointer to conjectures that imply the theorem.

share|improve this answer
add comment

I just read in a paper of Chalopin and Gonçalves (STOC '09) the following conjecture of West:

Every planar graph is the intersection graph of segments in the plane using only four directions.

Since parallel segments form an independent set in such a representation, this conjecture implies the 4CT, but perhaps is even stronger.

The reference: West, Open problems. SIAM J Discrete Math Newsletter, 2(1):10-12, 1991.

share|improve this answer
add comment

A snark is a connected, bridgeless cubic graph that is not 3-edge-colorable. Following wikipedia, the snark conjecture, generalizing the 4CT, is as follows:

Every snark has a subgraph that can be formed from the Petersen graph by subdividing some of its edges.

Again according to wikipedia, a proof of this conjecture was announced in 2001 by Robertson, Sanders, Seymour and Thomas.

share|improve this answer
    
Snark theorem doesn't seem to imply 4CT, right? –  Hsien-Chih Chang 張顯之 Apr 29 '11 at 1:10
    
It does in fact imply the 4CT: Every subdivision of the Petersen graph is clearly nonplanar, so the snark conjecture implies the following reformulation of the 4CT (due to Tait): Every snark is nonplanar. –  Hermann Gruber May 3 '11 at 6:34
1  
Ah, now I see where my problem is. The proof of the snark theorem is again a computer-aided proof. I'm under the impression that there's no human verifiable proof to the 4CT, and misunderstood your answer. Thanks!! –  Hsien-Chih Chang 張顯之 May 4 '11 at 5:19
add comment

As

L.H. Kauffman, Reformulating the map color theorem, Discrete Mathematics 302 (2005) 145–172

points out, the Primality Principle due to G. Spencer-Brown as well as the Eliahou–Kryuchkov conjecture are equivalent reformulations of the FCT.

  • S. Eliahou, Signed diagonal flips and the four color theorem, European J. Combin. 20 (1999) 641–646.
  • S. I. Kryuchkov, The four color theorem and trees, I. V. Kruchatov, Institute of Atomic Energy, Moscow, 1992, IAE-5537/1.
  • G. Spencer-Brown, Laws of Form, Gesetze der Form, Bohmeier Verlag, 1997.
share|improve this answer
add comment

Garry Bowlin and Matthew G. Brin's paper "Coloring Planar Graphs via Colored Paths in the Associahedra", last revised 12 May 2013, arXiv:1301.3984 math.CO contains the following conjecture on page 26:

Conjecture 6.4. For every pair of finite, binary trees (D, R) with the same number of leaves, there is a sign assignment of D and a word w of rotation symbols valid for D so that Dw = R.

It is stated that conjecture 6.4 following from previous propositions and theorems in the paper is equivalent to 4CT.

share|improve this answer
add comment

"The Face Labeling Of Maximal Planar Graphs" is the title of my old paper which has been published recently in which I have transformed 4 coloring of maximal planar graphs into consistency of face labeling. Link to the paper is http://www.math.nsysu.edu.tw/~amen/2011/091021-3.pdf

share|improve this answer
add comment

I am working on this:

If you can prove the theorem for rectangular maps, that are maps made from overlapping sheets of paper, you have also proved the 4ct. In addition, only maps with faces having all 5 edges or more can be considered in the search.

See http://4coloring.wordpress.com/ for details.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.