Four color theorem - AbsoluteAstronomy.com

Mathematics

Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...

, the four color theorem, or the four color map theorem states that, given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent

Adjacent

Adjacent is an adjective meaning contiguous, adjoining or abuttingIn geometry, adjacent is when sides meet to make an angle.In graph theory adjacent nodes in a graph are linked by an edge....

regions have the same color. Two regions are called adjacent only if they share a common boundary of non-zero length (i.e. other than a single point) that is not shared with a third region. For example, Utah

Utah

Utah is a state in the Western United States. It was the 45th state to join the Union, on January 4, 1896. Approximately 80% of Utah's 2,763,885 people live along the Wasatch Front, centering on Salt Lake City. This leaves vast expanses of the state nearly uninhabited, making the population the...

and Arizona

Arizona

Arizona ; is a state located in the southwestern region of the United States. It is also part of the western United States and the mountain west. The capital and largest city is Phoenix...

are adjacent, but Utah

Utah

and New Mexico

New Mexico

New Mexico is a state located in the southwest and western regions of the United States. New Mexico is also usually considered one of the Mountain States. With a population density of 16 per square mile, New Mexico is the sixth-most sparsely inhabited U.S...

, which only share a point that also belongs to Arizona

Arizona

Arizona ; is a state located in the southwestern region of the United States. It is also part of the western United States and the mountain west. The capital and largest city is Phoenix...

and Colorado

Colorado

Colorado is a U.S. state that encompasses much of the Rocky Mountains as well as the northeastern portion of the Colorado Plateau and the western edge of the Great Plains...

, are not.

Despite the motivation from coloring political maps of countries

Map coloring

Map coloring is the act of assigning different colors to different features on a map. There are two very different uses of this term. The first is in cartography, choosing the colors to be used when producing a map...

, the theorem is not of particular interest to mapmakers. According to an article by the math historian Kenneth May

Kenneth May

Kenneth O. May was an American mathematician and historian of mathematics, who developed May's theorem. The Kenneth O. May Prize is awarded for outstanding contributions to the history of mathematics....

, "Maps utilizing only four colours are rare, and those that do usually require only three. Books on cartography and the history of mapmaking do not mention the four-color property."

Three colors are adequate for simpler maps, but an additional fourth color is required for some maps, such as a map in which one region is surrounded by an odd number of other regions that touch each other in a cycle. The five color theorem

Five color theorem

The five color theorem is a result from graph theory that given a plane separated into regions, such as a political map of the counties of a state, the regions may be colored using no more than five colors in such a way that no two adjacent regions receive the same color.The five color theorem is...

, which has a short elementary proof, states that five colors suffice to color a map and was proven in the late 19th century ; however, proving that four colors suffice turned out to be significantly harder. A number of false proofs and false counterexample

Counterexample

In logic, and especially in its applications to mathematics and philosophy, a counterexample is an exception to a proposed general rule. For example, consider the proposition "all students are lazy"....

s have appeared since the first statement of the four color theorem in 1852.

The four color theorem was proven in 1976 by Kenneth Appel

Kenneth Appel

Kenneth Ira Appel is a mathematician who in 1976, with colleague Wolfgang Haken at the University of Illinois at Urbana-Champaign, solved one of the most famous problems in mathematics, the four-color theorem...

and Wolfgang Haken

Wolfgang Haken

Wolfgang Haken is a mathematician who specializes in topology, in particular 3-manifolds.In 1976 together with colleague Kenneth Appel at the University of Illinois at Urbana-Champaign, Haken solved one of the most famous problems in mathematics, the four-color theorem...

. It was the first major theorem

Theorem

In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...

to be proved using a computer. Appel and Haken's approach started by showing that there is a particular set of 1,936 maps, each of which cannot be part of a smallest-sized counterexample to the four color theorem. Appel and Haken used a special-purpose computer program to confirm that each of these maps had this property. Additionally, any map (regardless of whether it is a counterexample or not) must have a portion that looks like one of these 1,936 maps. Showing this required hundreds of pages of hand analysis. Appel and Haken concluded that no smallest counterexamples existed because any must contain, yet not contain, one of these 1,936 maps. This contradiction means there are no counterexamples at all and that the theorem is therefore true. Initially, their proof was not accepted by all mathematicians because the computer-assisted proof

Computer-assisted proof

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The idea is to use a computer program to perform lengthy computations, and...

was infeasible for a human to check by hand . Since then the proof has gained wider acceptance, although doubts remain .

To dispel remaining doubt about the Appel–Haken proof, a simpler proof using the same ideas and still relying on computers was published in 1997 by Robertson, Sanders, Seymour, and Thomas. Additionally in 2005, the theorem was proven by Georges Gonthier with general purpose theorem proving software

Automated theorem proving

Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...

Precise formulation of the theorem

The intuitive statement of the four color theorem, i.e. 'that given any separation of a 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', needs to be interpreted appropriately to be correct. For example, each region of the map should be contiguous.
In the real world, not all countries are contiguous

Enclave and exclave

In political geography, an enclave is a territory whose geographical boundaries lie entirely within the boundaries of another territory.An exclave, on the other hand, is a territory legally or politically attached to another territory with which it is not physically contiguous.These are two...

(e.g., Alaska

Alaska

Alaska is the largest state in the United States by area. It is situated in the northwest extremity of the North American continent, with Canada to the east, the Arctic Ocean to the north, and the Pacific Ocean to the west and south, with Russia further west across the Bering Strait...

as part of the United States

United States

The United States of America is a federal constitutional republic comprising fifty states and a federal district...

, Nakhchivan as part of Azerbaijan

Azerbaijan

Azerbaijan , officially the Republic of Azerbaijan is the largest country in the Caucasus region of Eurasia. Located at the crossroads of Western Asia and Eastern Europe, it is bounded by the Caspian Sea to the east, Russia to the north, Georgia to the northwest, Armenia to the west, and Iran to...

, and Kaliningrad

Kaliningrad Oblast

Kaliningrad Oblast is a federal subject of Russia situated on the Baltic coast. It has a population of The oblast forms the westernmost part of the Russian Federation, but it has no land connection to the rest of Russia. Since its creation it has been an exclave of the Russian SFSR and then the...

as part of Russia

Russia

Russia or , officially known as both Russia and the Russian Federation , is a country in northern Eurasia. It is a federal semi-presidential republic, comprising 83 federal subjects...

are not contiguous). Because the territory of a particular country must be the same color, four colors may not be sufficient. For instance, consider a simplified map:
In this map, the two regions labeled A belong to the same country, and must be the same color. This map then requires five colors, since the two A regions together are contiguous with four other regions, each of which is contiguous with all the others. If A consisted of three regions, six or more colors might be required; one can construct maps that require an arbitrarily high number of colors.

An easier to state version of the theorem uses graph theory

Graph theory

In mathematics and computer science, graph theory is the study of graphs, mathematical structures used to model pairwise relations between objects from a certain collection. A "graph" in this context refers to a collection of vertices or 'nodes' and a collection of edges that connect pairs of...

. The set of regions of a map can be represented more abstractly as an undirected graph that has a vertex

Vertex (graph theory)

In graph theory, a vertex or node is the fundamental unit out of which graphs are formed: an undirected graph consists of a set of vertices and a set of edges , while a directed graph consists of a set of vertices and a set of arcs...

for each region and an edge for every pair of regions that share a boundary segment. This graph is planar

Planar graph

In graph theory, a planar graph is a graph that can be embedded in the plane, i.e., it can be drawn on the plane in such a way that its edges intersect only at their endpoints...

: it can be drawn in the plane without crossings by placing each vertex at an arbitrarily chosen location within the region to which it corresponds, and by drawing the edges as curves that lead without crossing within each region from the vertex location to each shared boundary point of the region. Conversely any planar graph can be formed from a map in this way. In graph-theoretic terminology, the four-color theorem states that the vertices of every planar graph can be colored

Graph coloring

In graph theory, graph coloring is a special case of graph labeling; it is an assignment of labels traditionally called "colors" to elements of a graph subject to certain constraints. In its simplest form, it is a way of coloring the vertices of a graph such that no two adjacent vertices share the...

with at most four colors so that no two adjacent vertices receive the same color, or for short, "every planar graph is four-colorable" .

Early proof attempts

The conjecture

Conjecture

A conjecture is a proposition that is unproven but is thought to be true and has not been disproven. Karl Popper pioneered the use of the term "conjecture" in scientific philosophy. Conjecture is contrasted by hypothesis , which is a testable statement based on accepted grounds...

was first proposed in 1852 when Francis Guthrie

Francis Guthrie

Francis Guthrie was a South African mathematician and botanist who first posed the Four Colour Problem in 1852. At the time, Guthrie was a student of Augustus De Morgan at University College London. He studied under John Lindley, Professor of Botany at the University of London. Guthrie obtained...

, while trying to color the map of counties of England

England

England is a country that is part of the United Kingdom. It shares land borders with Scotland to the north and Wales to the west; the Irish Sea is to the north west, the Celtic Sea to the south west, with the North Sea to the east and the English Channel to the south separating it from continental...

, noticed that only four different colors were needed. At the time, Guthrie's brother, Fredrick, was a student of Augustus De Morgan

Augustus De Morgan

Augustus De Morgan was a British mathematician and logician. He formulated De Morgan's laws and introduced the term mathematical induction, making its idea rigorous. The crater De Morgan on the Moon is named after him....

at University College

University College London

University College London is a public research university located in London, United Kingdom and the oldest and largest constituent college of the federal University of London...

. Francis inquired with Fredrick regarding it, who then took it to De Morgan (Francis Guthrie graduated later in 1852, and later became a professor of mathematics in South Africa

South Africa

The Republic of South Africa is a country in southern Africa. Located at the southern tip of Africa, it is divided into nine provinces, with of coastline on the Atlantic and Indian oceans...

). According to De Morgan:

"A student of mine [Guthrie] asked me to day to give him a reason for a fact which I did not know was a fact — and do not yet. He says that if a figure be any how divided and the compartments differently coloured so that figures with any portion of common boundary line are differently coloured — four colours may be wanted but not more — the following is his case in which four colours are wanted. Query cannot a necessity for five or more be invented… "

The first published reference is by Arthur Cayley

Arthur Cayley

Arthur Cayley F.R.S. was a British mathematician. He helped found the modern British school of pure mathematics....

who in turn credits the conjecture to De Morgan .

There were several early failed attempts at proving the theorem

Theorem

In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...

. One proof

Mathematical proof

In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...

was given by Alfred Kempe

Alfred Kempe

Sir Alfred Bray Kempe D.C.L. F.R.S. was a mathematician best known for his work on linkages and the four color theorem....

in 1879, which was widely acclaimed; another was given by Peter Guthrie Tait

Peter Guthrie Tait

Peter Guthrie Tait FRSE was a Scottish mathematical physicist, best known for the seminal energy physics textbook Treatise on Natural Philosophy, which he co-wrote with Kelvin, and his early investigations into knot theory, which contributed to the eventual formation of topology as a mathematical...

in 1880. It was not until 1890 that Kempe's proof was shown incorrect by Percy Heawood, and 1891 Tait's proof was shown incorrect by Julius Petersen

Julius Petersen

Julius Peter Christian Petersen was a Danish mathematician.-Biography:Petersen's interests in mathematics were manifold .His famous paper Die Theorie der regulären graphs was a fundamental...

—each false proof stood unchallenged for 11 years .

In 1890, in addition to exposing the flaw in Kempe's proof, Heawood proved the five color theorem

Five color theorem

and generalized the four color conjecture to surfaces of arbitrary genus--see below.

Significant results were produced by Croatia

Croatia

Croatia , officially the Republic of Croatia , is a unitary democratic parliamentary republic in Europe at the crossroads of the Mitteleuropa, the Balkans, and the Mediterranean. Its capital and largest city is Zagreb. The country is divided into 20 counties and the city of Zagreb. Croatia covers ...

n mathematician Danilo Blanuša

Danilo Blanuša

Danilo Blanuša was a Croatian mathematician, physicist, engineer and a professor at the University of Zagreb. He was Serb and he was born in Austro-Ugarska monarchy ....

, who discovered two snarks

Snark (graph theory)

In the mathematical field of graph theory, a snark is a connected, bridgeless cubic graph with chromatic index equal to 4. In other words, it is a graph in which every vertex has three neighbors, and the edges cannot be colored by only three colors without two edges of the same color meeting at a...

in the 1940s, now known as Blanuša snarks

Blanuša snarks

In the mathematical field of graph theory, the Blanuša snarks are two 3-regular graphs with 18 vertices and 27 edges. They were discovered by Croatian mathematician Danilo Blanuša in 1946 and are named after him. When discovered, only one snark was known—the Petersen graph.As snarks, the Blanuša...

; prior to Blanuša's discovery, the only known snark was the Petersen graph

Petersen graph

In the mathematical field of graph theory, the Petersen graph is an undirected graph with 10 vertices and 15 edges. It is a small graph that serves as a useful example and counterexample for many problems in graph theory. The Petersen graph is named for Julius Petersen, who in 1898 constructed it...

(Weisstein).

In 1943, Hugo Hadwiger

Hugo Hadwiger

Hugo Hadwiger was a Swiss mathematician, known for his work in geometry, combinatorics, and cryptography.-Biography:...

formulated the Hadwiger conjecture

Hadwiger conjecture (graph theory)

In graph theory, the Hadwiger conjecture states that, if all proper colorings of an undirected graph G use k or more colors, then one can find k disjoint connected subgraphs of G such that each subgraph is connected by an edge to each other subgraph...

, a far-reaching generalization of the four-color problem that still remains unsolved.

Proof by computer

During the 1960s and 1970s German

Germany

Germany , officially the Federal Republic of Germany , is a federal parliamentary republic in Europe. The country consists of 16 states while the capital and largest city is Berlin. Germany covers an area of 357,021 km2 and has a largely temperate seasonal climate...

mathematician Heinrich Heesch

Heinrich Heesch

Heinrich Heesch was a German mathematician. He was born in Kiel and died in Hanover.In Göttingen he worked on Group theory. In 1933 Heesch witnessed the National Socialist purges among the university staff...

developed methods of using computer

Computer

A computer is a programmable machine designed to sequentially and automatically carry out a sequence of arithmetic or logical operations. The particular sequence of operations can be changed readily, allowing the computer to solve more than one kind of problem...

s to search for a proof. Notably he was the first to use discharging

Discharging method (discrete mathematics)

The discharging method is a technique used to prove lemmas in structural graph theory. Discharging is most well known for its central role in the proof of the Four Color Theorem. The discharging method is used to prove that every graph in a certain class contains some subgraph from a specified list...

for proving the theorem, which turned out to be important in the unavoidability portion of the subsequent Appel-Haken proof. He also expanded on the concept of reducibility and, along with Ken Durre, developed a computer test for it. Unfortunately, at this critical juncture, he was unable to procure the necessary supercomputer time to continue his work .

Others took up his methods and his computer-assisted approach. In 1976, while other teams of mathematicians were racing to complete proofs, Kenneth Appel

Kenneth Appel

and Wolfgang Haken

Wolfgang Haken

at the University of Illinois

University of Illinois at Urbana-Champaign

The University of Illinois at Urbana–Champaign is a large public research-intensive university in the state of Illinois, United States. It is the flagship campus of the University of Illinois system...

announced that they had proven the theorem. They were assisted in some algorithmic work by John A. Koch .

If the four-color conjecture were false, there would be at least one map with the smallest possible number of regions that requires five colors. The proof showed that such a minimal counterexample cannot exist, through the use of two technical concepts :

An unavoidable set contains regions such that every map must have at least one region from this collection.
A reducible configuration is an arrangement of countries that cannot occur in a minimal counterexample. If a map contains a reducible configuration, then the map can be reduced to a smaller map. This smaller map has the condition that if it can be colored with four colors, then the original map can also. This implies that if the original map can not be colored with four colors the smaller map can't either and so the original map is not minimal.

Using mathematical rules and procedures based on properties of reducible configurations, Appel and Haken found an unavoidable set of reducible configurations, thus proving that a minimal counterexample to the four-color conjecture could not exist. 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. This reducibility part of the work was independently double checked with different programs and computers. However, the unavoidability part of the proof was verified in over 400 pages of microfiche, which had to be checked by hand .

Appel and Haken's announcement was widely reported by the news media around the world, and the math department at the University of Illinois used a postmark stating "Four colors suffice." At the same time the unusual nature of the proof—it was the first major theorem to be proven with extensive computer assistance—and the complexity of the human verifiable portion, aroused considerable controversy .

In the early 1980s, rumors spread of a flaw in the Appel-Haken proof. Ulrich Schmidt at RWTH Aachen

RWTH Aachen

RWTH Aachen University is a research university located in Aachen, North Rhine-Westphalia, Germany with roughly 33,000 students enrolled in 101 study programs....

examined Appel and Haken's proof for his master's thesis . He had checked about 40% of the unavoidability portion and found a significant error in the discharging procedure . In 1986, Appel and Haken were asked by the editor of Mathematical Intelligencer

Mathematical Intelligencer

The Mathematical Intelligencer is a mathematical journal published by Springer Verlag that aims at a conversational and scholarly tone, rather than the technical and specialist tone more common amongst such journals.-Mathematical Conversations:...

to write an article addressing the rumors of flaws in their proof. They responded that the rumors were due to a "misinterpretation of [Schmidt's] results" and obliged with a detailed article . Their magnum opus, a book claiming a complete and detailed proof (with a microfiche supplement of over 400 pages), appeared in 1989 and explained Schmidt's discovery and several further errors found by others .

Simplification and verification

Since the proving of the theorem, efficient algorithms have been found for 4-coloring maps requiring only O

Big O notation

In mathematics, big O notation is used to describe the limiting behavior of a function when the argument tends towards a particular value or infinity, usually in terms of simpler functions. It is a member of a larger family of notations that is called Landau notation, Bachmann-Landau notation, or...

(n²) time, where n is the number of vertices. In 1996, Neil Robertson

Neil Robertson (mathematician)

G. Neil Robertson is a mathematician working mainly in topological graph theory, currently a distinguished professor at the Ohio State University. He earned his Ph.D. in 1969 at the University of Waterloo under his doctoral advisor William Tutte. According to the criteria of the Erdős Number...

, Daniel P. Sanders

Daniel P. Sanders

Daniel P. Sanders is known for his work a new efficient proof of proving the Four color theorem . He was formerly a guest professor of the department of computer science at Columbia University.Sanders received his Ph.D...

, Paul Seymour, and Robin Thomas

Robin Thomas (mathematician)

Robin Thomas is a mathematician working in graph theory at the Georgia Institute of Technology.Thomas received his doctorate in 1985 from Charles University in Prague, Czechoslovakia , under the supervision of Jaroslav Nešetřil...

created a quadratic time algorithm, improving on a quartic

Quartic function

In mathematics, a quartic function, or equation of the fourth degree, is a function of the formf=ax^4+bx^3+cx^2+dx+e \,where a is nonzero; or in other words, a polynomial of degree four...

algorithm based on Appel and Haken’s proof . This new proof is similar to Appel and Haken's but more efficient because it reduced the complexity of the problem and required checking only 633 reducible configurations. Both the unavoidability and reducibility parts of this new proof must be executed by computer and are impractical to check by hand . In 2001 the same authors announced an alternative proof, by proving the snark theorem .

In 2005 Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq

Coq

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification...

proof assistant. This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel .

Summary of proof ideas

The following discussion is a summary based on the introduction to Appel and Haken's book Every Planar Map is Four Colorable . Although flawed, Kempe's original purported proof of the four color theorem provided some of the basic tools later used to prove it. The explanation here is reworded in terms of the modern graph theory

Graph theory

formulation above.

Kempe's argument goes as follows. First, if planar regions separated by the graph are not triangulated, i.e. do not have exactly three edges in their boundaries, we can add edges without introducing new vertices in order to make every region triangular, including the unbounded outer region. If this triangulated graph

Planar graph

In graph theory, a planar graph is a graph that can be embedded in the plane, i.e., it can be drawn on the plane in such a way that its edges intersect only at their endpoints...

is colorable using four colors or less, so is the original graph since the same coloring is valid if edges are removed. So it suffices to prove the four color theorem for triangulated graphs to prove it for all planar graphs, and without loss of generality we assume the graph is triangulated.

Suppose v, e, and f are the number of vertices, edges, and regions. Since each region is triangular and each edge is shared by two regions, we have that 2e = 3f. This together with Euler's formula v − e + f = 2 can be used to show that 6v − 2e = 12. Now, the degree of a vertex is the number of edges abutting it. If v_n is the number of vertices of degree n and D is the maximum degree of any vertex,

But since 12 > 0 and 6 − i ≤ 0 for all i ≥ 6, this demonstrates that there is at least one vertex of degree 5 or less.

If there is a 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 d(v) ≤ 3, 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. As before we remove the vertex v and four-color the remaining vertices. If all four neighbors of v are different colors, say red, green, blue, and yellow in clockwise order, we look for an alternating path of vertices colored red and blue joining the red and blue neighbors. Such a path is called a Kempe chain

Kempe chain

In mathematics, a Kempe chain is a device used mainly in the study of the four colour theorem.-History:Kempe chains were first used by Alfred Kempe in his attempted proof of the four colour theorem. Even though his proof turned out to be incorrect, the method of Kempe chains is crucial to the...

. There may be a Kempe chain joining the red and blue neighbors, and there may be a Kempe chain joining the green and yellow neighbors, but not both, since these two paths would necessarily intersect, and the vertex where they intersect cannot be colored. Suppose it is the red and blue neighbors that are not chained together. Explore all vertices attached to the red neighbor by red-blue alternating paths, and then reverse the colors red and blue on all these vertices. The result is still a valid four-coloring, and v can now be added back and colored red.

This leaves only the case where G has a vertex of degree 5; but Kempe's argument was flawed for this case. Heawood noticed Kempe's mistake and also observed that if one was satisfied with proving only five colors are needed, one could run through the above argument (changing only that the minimal counterexample requires 6 colors) and use Kempe chains in the degree 5 situation to prove the five color theorem

Five color theorem

.

In any case, to deal with this degree 5 vertex case requires a more complicated notion than removing a vertex. Rather the form of the argument is generalized to considering configurations, which are connected subgraphs of G with the degree of each vertex (in G) specified. For example, the case described in degree 4 vertex situation is the configuration consisting of a single vertex labelled as having degree 4 in G. As above, it suffices to demonstrate that if the configuration is removed and the remaining graph four-colored, then the coloring can be modified in such a way that when the configuration is re-added, the four-coloring can be extended to it as well. A configuration for which this is possible is called a reducible configuration. If at least one of a set of configurations must occur somewhere in G, that set is called unavoidable. The argument above began by giving an unavoidable set of five configurations (a single vertex with degree 1, a single vertex with degree 2, ..., a single vertex with degree 5) and then proceeded to show that the first 4 are reducible; to exhibit an unavoidable set of configurations where every configuration in the set is reducible would prove the theorem.

Because G is triangular, the degree of each vertex in a configuration is known, and all edges internal to the configuration are known, the number of vertices in G adjacent to a given configuration is fixed, and they are joined in a cycle. These vertices form the ring of the configuration; a configuration with k vertices in its ring is a k-ring configuration, and the configuration together with its ring is called the ringed configuration. As in the simple cases above, one may enumerate all distinct four-colorings of the ring; any coloring that can be extended without modification to a coloring of the configuration is called initially good. For example, the single-vertex configuration above with 3 or less neighbors were initially good. In general, the surrounding graph must be systematically recolored to turn the ring's coloring into a good one, as was done in the case above where there were 4 neighbors; for a general configuration with a larger ring, this requires more complex techniques. Because of the large number of distinct four-colorings of the ring, this is the primary step requiring computer assistance.

Finally, it remains to identify an unavoidable set of configurations amenable to reduction by this procedure. The primary method used to discover such a set is the method of discharging

Discharging method (discrete mathematics)

. The intuitive idea underlying discharging is to consider the planar graph as an electrical network. Initially positive and negative "electrical charge" is distributed amongst the vertices so that the total is positive.

Recall the formula above:

Each vertex is assigned an initial charge of 6-deg(v). Then one "flows" the charge by systematically redistributing the charge from a vertex to its neighboring vertices according to a set of rules, the discharging procedure. Since charge is preserved, some vertices still have positive charge. The rules restrict the possibilities for configurations of positively-charged vertices, so enumerating all such possible configurations gives an unavoidable set.

As long as some member of the unavoidable set is not reducible, the discharging procedure is modified to eliminate it (while introducing other configurations). Appel and Haken's final discharging procedure was extremely complex and, together with a description of the resulting unavoidable configuration set, filled a 400-page volume, but the configurations it generated could be checked mechanically to be reducible. Verifying the volume describing the unavoidable configuration set itself was done by peer review over a period of several years.

A technical detail not discussed here but required to complete the proof is immersion reducibility.

False disproofs

The four color theorem has been notorious for attracting a large number of false proofs and disproofs in its long history. At first, The New York Times
The New York Times
The New York Times is an American daily newspaper founded and continuously published in New York City since 1851. The New York Times has won 106 Pulitzer Prizes, the most of any news organization...

refused as a matter of policy to report on the Appel–Haken proof, fearing that the proof would be shown false like the ones before it . Some alleged proofs, like Kempe's and Tait's mentioned above, stood under public scrutiny for over a decade before they were exposed. But many more, authored by amateurs, were never published at all.
Generally, the simplest, though invalid, counterexamples attempt to create one region which touches all other regions. This forces the remaining regions to be colored with only three colors. Because the four color theorem is true, this is always possible; however, because the person drawing the map is focused on the one large region, he fails to notice that the remaining regions can in fact be colored with three colors.

This trick can be generalized: there are many maps where if the colors of some regions are selected beforehand, it becomes impossible to color the remaining regions without exceeding four colors. A casual verifier of the counterexample may not think to change the colors of these regions, so that the counterexample will appear as though it is valid.

Perhaps one effect underlying this common misconception is the fact that the color restriction is not transitive

Transitive relation

In mathematics, a binary relation R over a set X is transitive if whenever an element a is related to an element b, and b is in turn related to an element c, then a is also related to c....

: a region only has to be colored differently from regions it touches directly, not regions touching regions that it touches. If this were the restriction, planar graphs would require arbitrarily large numbers of colors.

Other false disproofs violate the assumptions of the theorem in unexpected ways, such as using a region that consists of multiple disconnected parts, or disallowing regions of the same color from touching at a point.

Generalizations

The four-color theorem applies not only to finite planar graphs, but also to infinite graphs that can be drawn without crossings in the plane, and even more generally to infinite graphs (possibly with an uncountable number of vertices) for which every finite subgraph is planar. To prove this, one can combine a proof of the theorem for finite planar graphs with the De Bruijn–Erdős theorem stating that, if every finite subgraph of an infinite graph is k-colorable, then the whole graph is also k-colorable .

One can also consider the coloring problem on surfaces other than the plane

Plane (mathematics)

In mathematics, a plane is a flat, two-dimensional surface. A plane is the two dimensional analogue of a point , a line and a space...

(Weisstein). The problem on the sphere

Sphere

A sphere is a perfectly round geometrical object in three-dimensional space, such as the shape of a round ball. Like a circle in two dimensions, a perfect sphere is completely symmetrical around its center, with all points on the surface lying the same distance r from the center point...

or cylinder

Cylinder (geometry)

A cylinder is one of the most basic curvilinear geometric shapes, the surface formed by the points at a fixed distance from a given line segment, the axis of the cylinder. The solid enclosed by this surface and by two planes perpendicular to the axis is also called a cylinder...

is equivalent to that on the plane. For closed (orientable or non-orientable) surfaces with positive genus

Genus (mathematics)

In mathematics, genus has a few different, but closely related, meanings:-Orientable surface:The genus of a connected, orientable surface is an integer representing the maximum number of cuttings along non-intersecting closed simple curves without rendering the resultant manifold disconnected. It...

, the maximum number p of colors needed depends on the surface's Euler characteristic

Euler characteristic

In mathematics, and more specifically in algebraic topology and polyhedral combinatorics, the Euler characteristic is a topological invariant, a number that describes a topological space's shape or structure regardless of the way it is bent...

χ according to the formula

where the outermost brackets denote the floor function

Floor function

In mathematics and computer science, the floor and ceiling functions map a real number to the largest previous or the smallest following integer, respectively...

.

Alternatively, for an orientable surface the formula can be given in terms of the genus

Genus (mathematics)

of a surface, g:

(Weisstein).

This formula, the Heawood conjecture

Heawood conjecture

In graph theory, the Heawood conjecture or Ringel–Youngs theorem gives a lower bound for the number of colors that are necessary for graph coloring on a surface of a given genus. It was proven in 1968 by Gerhard Ringel and John W. T. Youngs. One case, the non-orientable Klein bottle, proved an...

, was conjectured by P.J. Heawood in 1890 and proven by Gerhard Ringel

Gerhard Ringel

Gerhard Ringel was a German mathematician who earned his Ph.D. from the University of Bonn in 1951...

and J. T. W. Youngs in 1968. The only exception to the formula is the Klein bottle

Klein bottle

In mathematics, the Klein bottle is a non-orientable surface, informally, a surface in which notions of left and right cannot be consistently defined. Other related non-orientable objects include the Möbius strip and the real projective plane. Whereas a Möbius strip is a surface with boundary, a...

, which has Euler characteristic 0 (hence the formula gives p = 7) and requires 6 colors, as shown by P. Franklin in 1934 (Weisstein).

For example, the torus

Torus

In geometry, a torus is a surface of revolution generated by revolving a circle in three dimensional space about an axis coplanar with the circle...

has Euler characteristic χ = 0 (and genus g = 1) and thus p = 7, so no more than 7 colors are required to color any map on a torus. The Szilassi polyhedron

Szilassi polyhedron

The Szilassi polyhedron is a nonconvex polyhedron, topologically a torus, with seven hexagonal faces.Each face of this polyhedron shares an edge with each other face. As a result, it requires seven colours to colour each adjacent face, providing the lower bound for the seven colour theorem...

is an example that requires seven colors.

A Möbius strip

Möbius strip

The Möbius strip or Möbius band is a surface with only one side and only one boundary component. The Möbius strip has the mathematical property of being non-orientable. It can be realized as a ruled surface...

also requires six colors (Weisstein).

There is no obvious extension of the coloring result to three-dimensional solid regions. By using a set of n flexible rods, one can arrange that every rod touches every other rod. The set would then require n colors, or n+1 if you consider the empty space that also touches every rod. The number n can be taken to be any integer, as large as desired. Such examples were known to Fredrick Gurthrie in 1880 . Even for axis-parallel cuboid

Cuboid

In geometry, a cuboid is a solid figure bounded by six faces, forming a convex polyhedron. There are two competing definitions of a cuboid in mathematical literature...

s (considered to be adjacent when two cuboids share a two-dimensional boundary area) an unbounded number of colors may be necessary .

Precise formulation of the theorem

Early proof attempts

Proof by computer

Simplification and verification

Summary of proof ideas

False disproofs

Generalizations

See also