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.

  • 6
    "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
  • ref for the stated conjecture? – vzn Aug 6 '14 at 16:33
  • A related question is asked over at mathoverflow: – Ian Agol Sep 10 '15 at 14:26

17 Answers 17

4CT is equivalent to:

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.

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:

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.

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.)

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

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.

Proposition 2.4 in this paper 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 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.

  • 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

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.

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.

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.

  • 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

"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


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.

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.

A k-flow on an undirected graph G is a directed graph derived by replacing each edge in G with an arc and assigning it an integer between -k and k, exclusive, such that, for each vertex in G, the sum of the integers assigned to arcs pointing into that vertex is equal to the sum of the integers assigned to arcs pointing out. A NWZ (nowhere zero) k-flow is a k-flow in which no arc has been assigned the number 0.

For any planar graph G, the dual of G is the graph that contains one vertex for each face in a planar embedding of G, and two vertices in a dual share one edge connecting them for every edge that the corresponding faces in G share between them in their boundaries. According to Tutte's Flow-Colouring Duality Theorem, a planar graph with no isthmus (i.e. edge whose deletion would increase the number of components) has a NWZ k-flow if and only if its dual is k-colourable. In other words, a planar graph is 4-colourable if and only if its dual has a NWZ 4-flow.

Note that 4CT requires the planar graph in question to have no loops (edges connecting any vertex to itself) because any graph with a loop cannot be vertex-coloured with any set of colours, since any vertex with a loop would therefore be adjacent to a vertex of the same colour, regardless of its colour.

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 for details.

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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