Editing Four color theorem (section)

==History==<!-- This section is linked from [[Mathematics]] -->

===Early proof attempts===
[[File:DeMorganFourColour.png|thumb|Letter of De Morgan to [[William Rowan Hamilton]], 23 Oct. 1852]]
As far as is known,<ref>There is some mathematical folk-lore that [[August Ferdinand Möbius|Möbius]] originated the four-color conjecture, but this notion seems to be erroneous. See {{citation|title=Graph Theory, 1736–1936|title-link=Graph Theory, 1736–1936|author=Biggs, Norman|author-link=Norman L. Biggs|author2=Lloyd, E. Keith|author3=Wilson, Robin J.|author-link3=Robin Wilson (mathematician)|year=1986|publisher=Oxford University Press|isbn=0-19-853916-9|at=[https://books.google.com/books?id=XqYTk0sXmpoC&pg=PA116 p. 116]}} & {{citation|title=Note on the history of the map-coloring problem|author=Maddison, Isabel|author-link=Isabel Maddison|journal=Bull. Amer. Math. Soc.|volume=3|issue=7|year=1897|page=257|doi=10.1090/S0002-9904-1897-00421-9|doi-access=free}}</ref> the conjecture was first proposed on October 23, 1852,<ref name=MacKenzie>Donald MacKenzie, ''Mechanizing Proof: Computing, Risk, and Trust'' (MIT Press, 2004) p103</ref> when [[Francis Guthrie]], while trying to color the map of counties of England, noticed that only four different colors were needed. At the time, Guthrie's brother, [[Frederick Guthrie (scientist)|Frederick]], was a student of [[Augustus De Morgan]] (the former advisor of Francis) at [[University College London]]. Francis inquired with Frederick 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.) According to De Morgan:

<blockquote>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 colored so that figures with any portion of common boundary ''line'' are differently colored—four colors may be wanted but not more—the following is his case in which four colors ''are'' wanted. Query cannot a necessity for five or more be invented...{{sfnp|Wilson|2014|p=12}}</blockquote>

"F.G.", perhaps one of the two Guthries, published the question in ''[[Athenaeum (British magazine)|The Athenaeum]]'' in 1854,<ref>{{harvtxt|F. G.|1854}}; {{harvtxt|McKay|2012}}</ref> and De Morgan posed the question again in the same magazine in 1860.<ref name=Athenaeum1860>{{citation|journal=[[Athenaeum (British magazine)|The Athenaeum]]|date=April 14, 1860|first=Augustus|last=De Morgan (anonymous)|author-link=Augustus De Morgan|pages=501–503|title=The Philosophy of Discovery, Chapters Historical and Critical. By W. Whewell.}}</ref> Another early published reference by {{harvs|first=Arthur|last=Cayley|authorlink=Arthur Cayley|year=1879|txt}} in turn credits the conjecture to De Morgan.

There were several early failed attempts at proving the theorem. De Morgan believed that it followed from a simple fact about four regions, though he didn't believe that fact could be derived from more elementary facts.
<blockquote>This arises in the following way. We never need four colours in a neighborhood unless there be four counties, each of which has boundary lines in common with each of the other three. Such a thing cannot happen with four areas unless one or more of them be inclosed by the rest; and the colour used for the inclosed county is thus set free to go on with. Now this principle, that four areas cannot each have common boundary with all the other three without inclosure, is not, we fully believe, capable of demonstration upon anything more evident and more elementary; it must stand as a postulate.<ref name=Athenaeum1860 /></blockquote>

One proposed proof was given by [[Alfred Kempe]] in 1879, which was widely acclaimed;<ref name="rouse_ball_1960">[[W. W. Rouse Ball]] (1960) ''The Four Color Theorem'', in Mathematical Recreations and Essays, Macmillan, New York, pp 222–232.</ref> another was given by [[Peter Guthrie Tait]] in 1880. It was not until 1890 that Kempe's proof was shown incorrect by [[Percy Heawood]], and in 1891, Tait's proof was shown incorrect by [[Julius Petersen]]—each false proof stood unchallenged for 11 years.{{sfnp|Thomas|1998|p=848}}

In 1890, in addition to exposing the flaw in Kempe's proof, Heawood proved the [[five color theorem]] and generalized the four color conjecture to surfaces of arbitrary genus.{{sfnp|Heawood|1890}}

Tait, in 1880, showed that the four color theorem is equivalent to the statement that a certain type of graph (called a [[snark (graph theory)|snark]] in modern terminology) must be non-[[planar graph|planar]].{{sfnp|Tait|1880}}

In 1943, [[Hugo Hadwiger]] formulated the [[Hadwiger conjecture (graph theory)|Hadwiger conjecture]],{{sfnp|Hadwiger|1943}} a far-reaching generalization of the four-color problem that still remains unsolved.

===Proof by computer===
During the 1960s and 1970s, German mathematician [[Heinrich Heesch]] developed methods of using computers to search for a proof. Notably he was the first to use [[discharging method (discrete mathematics)|discharging]] 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.{{sfnp|Wilson|2014|pp=139–142}}

Others took up his methods, including his computer-assisted approach. While other teams of mathematicians were racing to complete proofs, [[Kenneth Appel]] and [[Wolfgang Haken]] at the [[University of Illinois at Urbana–Champaign|University of Illinois]] announced, on June 21, 1976,<ref>Gary Chartrand and Linda Lesniak, ''Graphs & Digraphs'' (CRC Press, 2005) p.221</ref> that they had proved the theorem. They were assisted in some algorithmic work by [[John A. Koch]].{{sfnp|Wilson|2014|pp=145–146}}

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:<ref>{{harvtxt|Wilson|2014|pp=105–107}}; {{harvtxt|Appel|Haken|1989}}; {{harvtxt|Thomas|1998|pp=852–853}}</ref>

# An ''unavoidable set'' is a set of configurations such that every map that satisfies some necessary conditions for being a minimal non-4-colorable [[maximal planar graph|triangulation]] (such as having minimum degree 5) must have at least one configuration from this set.
# A ''reducible configuration'' is an arrangement of countries that cannot occur in a minimal counterexample. If a map contains a reducible configuration, the map can be reduced to a smaller map. This smaller map has the condition that if it can be colored with four colors, this also applies to the original map. This implies that if the original map cannot be colored with four colors the smaller map cannot 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,834 reducible configurations (later reduced to 1,482) 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 with the assistance of Haken's daughter [[Dorothea Blostein]].{{sfnp|Appel|Haken|1989}}

Appel and Haken's announcement was widely reported by the news media around the world,{{sfnp|Wilson|2014|p=153}} and the math department at the [[University of Illinois]] used a postmark stating "Four colors suffice."{{sfnp|Wilson|2014|p=150}} At the same time the unusual nature of the proof—it was the first major theorem to be proved with extensive computer assistance—and the complexity of the human-verifiable portion aroused considerable controversy.{{sfnp|Wilson|2014|p=157}}

In the early 1980s, rumors spread of a flaw in the Appel&ndash;Haken proof. Ulrich Schmidt at [[RWTH Aachen]] had examined Appel and Haken's proof for his master's thesis that was published in 1981.{{sfnp|Wilson|2014|p=165}} He had checked about 40% of the unavoidability portion and found a significant error in the discharging procedure {{Harv|Appel|Haken|1989}}. In 1986, Appel and Haken were asked by the editor of ''[[Mathematical Intelligencer]]'' to write an article addressing the rumors of flaws in their proof. They replied that the rumors were due to a "misinterpretation of [Schmidt's] results" and obliged with a detailed article.{{sfnp|Wilson|2014|p=165}} Their [[Masterpiece|magnum opus]], ''Every Planar Map is Four-Colorable'', a book claiming a complete and detailed proof (with a microfiche supplement of over 400 pages), appeared in 1989; it explained and corrected the error discovered by Schmidt as well as several further errors found by others.{{sfnp|Appel|Haken|1989}}

===Simplification and verification===
Since the proving of the theorem, a new approach has led to both a shorter proof and a more efficient algorithm for 4-coloring maps. In 1996, [[Neil Robertson (mathematician)|Neil Robertson]], [[Daniel P. Sanders]], [[Paul Seymour (mathematician)|Paul Seymour]], and [[Robin Thomas (mathematician)|Robin Thomas]] created a [[polynomial time|quadratic-time]] algorithm (requiring only [[Big O notation|O]](''n''<sup>2</sup>) time, where ''n'' is the number of vertices), improving on a [[quartic function|quartic]]-time algorithm based on Appel and Haken's proof.<ref>{{harvtxt|Thomas|1995}}; {{harvtxt|Robertson|Sanders|Seymour|Thomas|1996}}.</ref> The new proof, based on the same ideas, is similar to Appel and Haken's but more efficient because it reduces the complexity of the problem and requires checking only 633 reducible configurations. Both the unavoidability and reducibility parts of this new proof must be executed by a computer and are impractical to check by hand.{{sfnp|Thomas|1998|pp=852–853}} In 2001, the same authors announced an alternative proof, by proving the [[snark conjecture]].<ref>{{harvtxt|Thomas|1999}}; {{harvtxt|Pegg|Melendez|Berenguer|Sendra|2002}}.</ref> This proof remains unpublished, however.

In 2005, [[Benjamin Werner]] and [[Georges Gonthier]] formalized a proof of the theorem inside the [[Coq (software)|Coq]] 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.{{sfnp|Gonthier|2008}}