Xiangs formal proof of the four color theorem [605452]

Xiang’s formal proof of the four color theorem
– 1 –

A formal proof of the four color theorem
Limin Xiang
Department of Information Science,
Kyushu Sangyo University
3-1 Matsukadai 2-Chome, Higashi-ku, Fukuoka 813-8503, Japan E-mail: [anonimizat]

Tel: +81-92-673-5400, Fax: +81-92-673-5454
Manuscript, April 16, 2009

Abstract : A formal proof has not been found for the four co lor theorem since 1852 when Francis Guthrie first
conjectured the four color theorem. Why? A bad idea, we think, directed people to a rough road. Using a similar
method to that for the formal proof of the five color theorem, a formal proof is proposed in this paper of the four color
theorem, namely, every planar graph is four-colorable. The formal proof proposed can also be regarded as an
algorithm to color a planar graph using four colors so that no two adjacent vertices receive the same color.

1. Introduction

Since 1852 when Francis Guthrie first conjectured
the four color theorem [1], a formal proof has not been
found for the four color theorem. The four color
theorem , or the four color map theorem , states that
given any separation of the plane into contiguous

regions, called a "map", the regions can be colored
using at most four colors so that no two adjacent regions have the same color. Two regions are called
adjacent only if they share a border segment, not just
a point. To precisely state the theorem, it is easiest to rephrase it in graph theory . It then states that the
vertices of every planar graph can be coloured with at
most four colors so that no two adjacent vertices receive the same color, or "every planar graph is four-
colorable" for short. Such a graph can be obtained
from a map by replacing every region by a vertex, and connecting two vertices by an edge exactly when the
two regions share a border segment (not just a corner.)
[1].

A computer-assisted proof of the four color theorem
was proposed by Kenneth Appel and Wolfgang Haken
in 1976. Their proof reduced the infinitude of possible
maps to 1,936 reducible configurations (later reduced to 1,476) which had to be checked one by one by
computer and took over a thousand hours [1].
However, because part of the proof consisted of an
exhaustive analysis of many discrete cases by a
computer, some mathematicians do not accept it [2].

A graph
G consists of a non-empty finite set V of
vertices and a finite set E of edges on V, i.e., any
edge of E connects two vertices of V. If vertex v is
shared by k edges, k is called the degree of vertex
v, and denoted by kvd =)( .
A planar graph G is a Graph that may be embedded
in the plane without intersecting edges.

A graph G is said to be n-colorable , denoted by
n Gc =)( , if it's possible to assign one of n colors to
each vertex in such a way that no two connected
vertices have the same color.
More than 150 years passed, but a formal proof has
not been found for the four color theorem. Why? The following idea [1], we think, directed people to a bumpy road.
If there is a maximal planar graph requiring
5 colors, then there is a minimal such graph,
where removing any vertex makes it four-
colorable. Call this graph
G. G cannot
have a vertex of degree 3 or less, because if
3)(≤vd , we can remove v from G, four-
color the smaller graph, then add back v
and extend the four-coloring to it by
choosing a color different from its neighbors.
Kempe also showed correctly that G can
have no vertex of degree 4.
The minimal graph G above does not exist, if the
four color theorem holds. Any research on the
inexistent minimal graph G should be not only very
difficult and inefficient, but also too hard to understand.
Kenneth Appel and Wolfgang Haken’s computer-assisted proof is just such an example.
In fact, the four color theorem holds, so we may
prove it directly. Using a similar method to that for the formal proof of the five color theorem [3], a formal
proof of the four color t heorem is proposed in this

Xiang’s formal proof of the four color theorem
– 2 –
paper. In Section 2, some notations are introduced,
and the formal proof of the four color theorem is given
in Section 3. A hand-checked case flow chart is shown
in Section 4 for the proof, which can be regarded as an algorithm to color a planar graph using four colors so
that no two adjacent vertices receive the same color.
Section 5 concludes the paper.
2. Notations
Given a graph
G and a vertex v in G, vG− is the
graph removing v and all its shared edges from G.
The reverse of vG− is vvG +−) ( , and
GvvG =+−) ( .
),(jiG is a subgraph of G consisting of the vertices
that are colored with colors i and j only, and edges
connecting two of them. ),,(vjiGc is the connected
component of ),(jiG containing vertex v.
A path in ),(jiG , called a Kempe chain and denoted
by ),,,( vujiCh , joining vertices u and v, that is a
sequence of edges and vertices painted only with
colors i and j.
v is a vertex of graph G, which is denoted by Gv∈ ,
and on the contrary v is not a vertex of graph G,
which is denoted by Gv∉ .

A circle is a closed path. When vertex
),,,( vujiChw∉ , ),,,( vujiCh together with w as
well as its two edges connected to u and v forms a
Kempe circle , which is denoted by wvujiCh +),,,( .
Suppose )(vn , )(en , and )(fn are the number of
vertices, edges, and faces in a planar graph. Since
each edge is shared by two faces and each face is
bounded by three edges at least, )(3)(2 fn en≥
which together with Euler's formula
2)()()( = + − fnenvn can be used to show
12)(2)(6 ≥ − en vn . Now, if )(idn is the number of
vertices of degree id and D is the maximum degree,
with Euler’s Theorem )( )(2
1∑
=× =D
iidni en , .12)()6()( )( 6)(2)(6
111
≥ − =× − = −
∑∑∑
===
D
iiiD
iD
ii
dnidni dn en vn

But since 0 12> and 0 6 ≤−i for all 6≥i , this
demonstrates that there is at least one vertex of
degree 5 or less in a planar graph [1]. Thus, the following lemma holds.
Lemma 1. For any planar graph
nG with n ( 6≥n )
vertices, there are vertices nv, 1−nv, …, 6v such
that 5)(≤ivd and i i i vG G − =−1 are also planar
graphs for i from n down to 6.
Thus, the formal proof of the four color theorem can be
given in the following section.
3. The proof
Theorem 1(The Four color Theorem ) Every planar
graph is four-colorable.
Proof. Let the planar graph be with n vertices, where
1≥n , and denoted by nG. There are 3 cases
(Case.1 – Case.3) to discuss.
Case.1 : When 4 1 ≤≤n , the result holds obviously.
Case.2 : When 5=n , the maximal planar graph with
5 vertices is the full graph deleting an edge, i.e., the
planar graph with 5 vertices and 9 edges, which is
denoted by '5G. Any 5G is a subgraph of '5G, and
)'()(5 5 Gc Gc ≤ . Since 4)'(5=Gc (see, for
example, Fig. 1(a), ) 4)(5=Gc , i.e., the result
holds.
Case.3 : When 6≥n , by Lemma 1, there are vertices
nv, 1−nv , …, 6v such that 5)(≤ivd and
i i i vG G − =−1 are also planar graphs for i from n
down to 6.
It will be shown that 4) ()(1 = + =− i i i v Gc Gc for i
from 6 up to n in the following.
For i from 6 up to n, since 4)(5=Gc by Case.2,
let 4) (1=−iGc , and

Xiang’s formal proof of the four color theorem
– 3 –
)({)( uc vCi= | )(uc is the color of vertex u
in 1−iG, and u is adjacent to iv in iG}
Note that 4)(≤ivC and 5)( )( ≤ ≤i i vd vC . There
are 3 cases (Case.3.1 – Case.3.3) to discuss.
Case.3.1 : 3|)(| ≤ivC , let iv be colored with the 4th
color, and 4)(=iGc . The result holds.
Case.3.2: 4|)(| =ivC and 4)(=ivd , let
1v,2v,3v,4v be adjacent to iv in clockwise order,
and j vcj=)( for 4 1 ≤≤j without loss of
generality. Consider the subgraph )3,1(iG of iG,
there are 2 cases (Case.3.2.1, Case.3.2.2) to
discuss.
Case.3.2.1 : ),3,1(3 1 v Gvc
i∉ (see, for example, Fig.
1(b),) we can reverse the coloration on ),3,1(3v Gc
i ,
thus assigning color number 3 to iv and completing
the task.
Case.3.2.2 : ),3,1(3 1 v Gvc
i∈ , we can find a Kempe
chain ),,3,1(3 1vv Ch in )3,1(iG (see, for example,
Fig. 1(c).) Kempe Circle iv vv Ch +),,3,1(3 1
separates ),4,2(2v Gc
i of )4,2(iG from
),4,2(4v Gc
i , we can reverse the coloration on
),4,2(2v Gc
i , thus assigning color number 2 to iv
and completing the task.
Thus, the result holds in Case.3.2.
Case.3.3 : 4|)(| =ivC and 5)(=ivd , let
1v,2v,3v,4v,5v be adjacent to iv in clockwise
order. Only two of the five vertices are painted with
the same color, and the two vertices with the same color are neighbor or isolate in cyclic order.
Therefore, there are 2 cases (Case.3.3.1,
Case.3.3.2) to discuss.
Case.3.3.1 : The two vertices with the same color are
neighbor in cyclic order, without loss of generality,
let
j vcj=)( for 4 1 ≤≤j and 1)(5=vc . Consider the subgraph )3,1(iG of iG, there are 2 cases
(Case.3.3.1.1, Case.3.3.1.2) to discuss.
Case.3.3.1.1 : ),3,1(1 3 v Gvc
i∉ and ),3,1(5 3 v Gvc
i∉
(see, for example, Fig. 1(d),) we can reverse the
coloration on ),3,1(3v Gc
i , thus assigning color
number 3 to iv and completing the task.
Case.3.3.1.2 : ),3,1(1 3 v Gvc
i∈ or ),3,1(5 3 v Gvc
i∈ , we
can find a Kempe chain ),,3,1(3 1vv Ch or
),,3,1(3 5vv Ch in )3,1(iG (see, for example, Fig.
1(e).) Kempe Circle iv vv Ch +),,3,1(3 1 or
iv vv Ch +),,3,1(3 5 separates ),4,2(2v Gc
i of
)4,2(iG from ),4,2(4v Gc
i , we can reverse the
coloration on ),4,2(2v Gc
i , thus assigning color
number 2 to iv and completing the task.
Thus, the result holds in Case.3.3.1.
Case.3.3.2 : The two vertices with the same color are
isolate in cyclic order, wi thout loss of generality, let
1)()(3 1 = =vc vc , 2)(2=vc , 3)(4=vc , and
4)(5=vc . Consider the subgraph )4,2(iG of iG,
there are 2 cases (Case.3.3.2.1, Case.3.3.2.2) to
discuss.
Case.3.3.2.1 : ),4,2(5 2 v Gvc
i∉ (see, for example, Fig.
1(f),) we can reverse the coloration on ),4,2(5v Gc
i ,
thus assigning color number 4 to iv and
completing the task.
Case.3.3.2.2 : ),4,2(5 2 v Gvc
i∈ . There are 2 cases
(Case.3.3.2.2.1, Case.3.3.2.2.2) to discuss.
Case.3.3.2.2.1 : ),3,2(4 2 v Gvc
i∉ (see, for example,
Fig. 1(g),) we can reverse the coloration on
),3,2(4v Gc
i , thus assigning color number 3 to iv
and completing the task.
Case.3.3.2.2.2 : ),3,2(4 2 v Gvc
i∈ , we can find a
Kempe chain ),,3,2(4 2vv Ch in )3,2(iG (see, for
example, Fig.1(h).) Kempe circle
iv vv Ch +),,3,2(4 2 separates ),4,1(3v Gc
i of

Xiang’s formal proof of the four color theorem
– 4 –
)4,1(iG from ),4,1(5v Gc
i , we can reverse the
coloration on ),4,1(3v Gc
i . Then (see, for example,
Fig. 1(i),) we can find a Kempe chain
),,4,2(5 2vv Ch in )4,2(iG . Kempe circle
iv vv Ch +),,4,2(5 2 separates ),3,1(1v Gc
i of
)3,1(iG from ),3,1(4v Gc
i , we can reverse the
coloration on ),3,1(1v Gc
i , thus assigning color
number 1 to iv and completing the task (see, for
example, Fig. 1(j).)
Thus, 4) ()(1 = + =− i i i v Gc Gc , since 4) (1=−iGc .
By Mathematical induction , the result holds for all
cases.
Therefore, the proof is completed.
4. The flow chart
A hand-checked case flow chart is shown in Fig. 2
for the proof in Section 3.

5. Conclusions
The hand-checked case flow chart shown in Section
4 can be regarded as an algorithm to color a planar
graph using four colors so that no two adjacent
vertices receive the same color.
Since the four color theorem holds, it can be proved
directly. Using a similar method to that for the formal
proof of the five color theorem [3], a formal proof of the
four color theorem was proposed in this paper.

References
[1] http://en.wikipedia.org/wiki/Four_color_theorem

[2] http://mathworld.w olfram.com/Four-
ColorTheorem.html
[3] http://en.wikipedia.org/wiki/Five_color_theorem

Xiang’s formal proof of the four color theorem
– 5 –
a
223
41
b 2=c(v )
3=c(v )
4=c(v )1=c(v )12
3
4c(v )i

c 2=c(v )
3=c(v )
4=c(v )1=c(v )12
3
4c(v )i
d 2=c(v )
3=c(v )
4=c(v )1=c(v )12
3
4c(v )i
1=c(v )5
ｅ 2=c(v )
3=c(v )
4=c(v )1=c(v )12
3
4c(v )i
1=c(v )5
f 2=c(v )
1=c(v )
3=c(v )1=c(v )12
3
4c(v )i
4=c(v )5
g 2=c(v )
1=c(v )
3=c(v )1=c(v )12
3
4c(v )i
4=c(v )5 h 2=c(v )
1=c(v )
3=c(v )1=c(v )12
3
4c(v )i
4=c(v )5
i 2=c(v )
4=c(v )
3=c(v )1=c(v )12
3
4c(v )i
4=c(v )5 j 2=c(v )
4=c(v )
3=c(v )3=c(v )12
3
4c(v )i
4=c(v )5=1

Fig.1 . For cases of the prof

Xiang’s formal proof of the four color theorem
– 6 –

Fig. 2. The flow chart for the proof