History Four color theorem

1 history

1.1 proof attempts
1.2 proof computer
1.3 simplification , verification

history
early proof attempts

letter of de morgan hamilton, 23 oct. 1852

as far known, conjecture first proposed on october 23, 1852 when francis guthrie, while trying color map of counties of england, noticed 4 different colors needed. @ time, guthrie s brother, frederick, student of augustus de morgan (the former advisor of francis) @ university college london. francis inquired frederick regarding it, took de morgan (francis guthrie graduated later in 1852, , later became professor of mathematics in south africa). according de morgan:

student of mine [guthrie] asked me day give him reason fact did not know fact—and not yet. says if figure how divided , compartments differently colored figures portion of common boundary line differently colored—four colors may wanted not more—the following case in 4 colors wanted. query cannot necessity 5 or more invented… (wilson 2014, p. 18)

f.g. , perhaps 1 of 2 guthries, published question in athenaeum in 1854, , de morgan posed question again in same magazine in 1860. published reference arthur cayley (1879) in turn credits conjecture de morgan.

there several failed attempts @ proving theorem. de morgan believed followed simple fact 4 regions, though didn t believe fact derived more elementary facts.

this arises in following way. never need 4 colors in neighborhood unless there 4 counties, each of has boundary lines in common each of other three. such thing cannot happen 4 areas unless 1 or more of them inclosed rest; , color used inclosed county set free go on with. principle, 4 areas cannot each have common boundary other 3 without inclosure, not, believe, capable of demonstration upon more evident , more elementary; must stand postulate.

one alleged proof given alfred kempe in 1879, acclaimed; given peter guthrie tait in 1880. not until 1890 kempe s proof shown incorrect percy heawood, , in 1891, tait s proof shown incorrect julius petersen—each false proof stood unchallenged 11 years (thomas 1998, p. 848).

in 1890, in addition exposing flaw in kempe s proof, heawood proved 5 color theorem (heawood 1890) , generalized 4 color conjecture surfaces of arbitrary genus—see below.

tait, in 1880, showed 4 color theorem equivalent statement type of graph (called snark in modern terminology) must non-planar.

in 1943, hugo hadwiger formulated hadwiger conjecture (hadwiger 1943), far-reaching generalization of four-color problem still remains unsolved.

proof computer

during 1960s , 1970s german mathematician heinrich heesch developed methods of using computers search proof. notably first use discharging proving theorem, turned out important in unavoidability portion of subsequent appel-haken proof. expanded on concept of reducibility and, along ken durre, developed computer test it. unfortunately, @ critical juncture, unable procure necessary supercomputer time continue work (wilson 2014).

others took methods , computer-assisted approach. while other teams of mathematicians racing complete proofs, kenneth appel , wolfgang haken @ university of illinois announced, on june 21, 1976, had proved theorem. assisted in algorithmic work john a. koch (wilson 2014).

if four-color conjecture false, there @ least 1 map smallest possible number of regions requires 5 colors. proof showed such minimal counterexample cannot exist, through use of 2 technical concepts (wilson 2014; appel & haken 1989; thomas 1998, pp. 852–853):

using mathematical rules , procedures based on properties of reducible configurations, appel , haken found unavoidable set of reducible configurations, proving minimal counterexample four-color conjecture not exist. proof reduced infinitude of possible maps 1,936 reducible configurations (later reduced 1,476) had checked 1 one computer , took on thousand hours. reducibility part of work independently double checked different programs , computers. however, unavoidability part of proof verified in on 400 pages of microfiche, had checked hand assistance of haken s daughter dorothea blostein (appel & haken 1989).

appel , haken s announcement reported news media around world, , math department @ university of illinois used postmark stating 4 colors suffice. @ same time unusual nature of proof—it first major theorem proved extensive computer assistance—and complexity of human-verifiable portion, aroused considerable controversy (wilson 2014).

in 1980s, rumors spread of flaw in appel-haken proof. ulrich schmidt @ rwth aachen examined appel , haken s proof master s thesis (wilson 2014, 225). had checked 40% of unavoidability portion , found significant error in discharging procedure (appel & haken 1989). in 1986, appel , haken asked editor of mathematical intelligencer write article addressing rumors of flaws in proof. responded rumors due misinterpretation of [schmidt s] results , obliged detailed article (wilson 2014, 225–226). magnum opus, every planar map four-colorable, book claiming complete , detailed proof (with microfiche supplement of on 400 pages), appeared in 1989 , explained schmidt s discovery , several further errors found others (appel & haken 1989).

simplification , verification

since proving of theorem, efficient algorithms have been found 4-coloring maps requiring o(n) time, n number of vertices. in 1996, neil robertson, daniel p. sanders, paul seymour, , robin thomas created quadratic-time algorithm, improving on quartic-time algorithm based on appel , haken’s proof (thomas 1995; robertson et al. 1996). new proof similar appel , haken s more efficient because reduces complexity of problem , requires checking 633 reducible configurations. both unavoidability , reducibility parts of new proof must executed computer , impractical check hand (thomas 1998, pp. 852–853). in 2001, same authors announced alternative proof, proving snark theorem (thomas; pegg et al. 2002).

in 2005, benjamin werner , georges gonthier formalized proof of theorem inside coq proof assistant. removed need trust various computer programs used verify particular cases; necessary trust coq kernel.