Celebratio Mathematica

Wolfgang Haken

The solution of the four-color-map problem

by Kenneth Appel and Wolfgang Haken

In 1852, a few months after he had com­pleted his stud­ies at Uni­versity Col­lege Lon­don, Fran­cis Gu­thrie wrote a let­ter to his broth­er Fre­d­er­ick, who was still at the col­lege as a stu­dent of the math­em­atician Au­gus­tus De Mor­gan. Fran­cis poin­ted out to Fre­d­er­ick that it seemed that every map drawn on a sheet of pa­per can be colored with only four col­ors in such a way that coun­tries shar­ing a com­mon bor­der have dif­fer­ent col­ors. He asked if there was any way to prove this math­em­at­ic­ally. Fre­d­er­ick did not know, and he asked De Mor­gan, who did not know either. For the next 124 years Gu­thrie’s four-col­or prob­lem, the prob­lem of prov­ing that every map re­quires at most four col­ors or of draw­ing a map that re­quires five col­ors, in­trigued pro­fes­sion­al math­em­aticians, am­a­teur math­em­aticians and high school stu­dents who felt that all un­solved prob­lems re­main so only be­cause of the in­com­pet­ence of the older gen­er­a­tion.

Figure 1. Four-Color Theorem states that four colors are always sufficient to color a planar map so that no two neighboring countries are the same color. For the theorem to make sense a map must consist of contiguous countries. Neighboring countries must be adjacent along a line, because if countries adjacent at single points were considered neighbors, then map at the left would require a different color for each of its seven countries. Country must be a single connected region, otherwise map at right, with country \( E \) in two pieces, would require five colors.

In 1976 we solved the four-col­or prob­lem. Gu­thrie’s con­jec­ture was proved math­em­at­ic­ally, but in a way quite dif­fer­ent from what he might have ex­pec­ted. Even among present-day math­em­aticians those who were not aware of the de­vel­op­ments lead­ing to the proof are rather dis­mayed by the res­ult be­cause the proof made un­pre­ced­en­ted use of com­puters; the com­pu­ta­tions of the proof make it longer than has tra­di­tion­ally been con­sidered ac­cept­able. In fact, the cor­rect­ness of the proof can­not be checked without the aid of a com­puter. Moreover, some of the cru­cial ideas of the proof were per­fec­ted by com­puter ex­per­i­ments. Of course, a short proof of the four-col­or the­or­em may some day be found, per­haps by one of those bright high school stu­dents. It is also con­ceiv­able that no such proof is pos­sible. In this case a new and in­ter­est­ing type of the­or­em has ap­peared, one which has no proof of the tra­di­tion­al type.

In spite of the nov­el as­pects of the proof, both the four-col­or prob­lem and the ba­sic meth­od of proof have deep roots in math­em­at­ics. We will be­gin to ex­am­ine them by re­turn­ing to the ini­tial for­mu­la­tion of the prob­lem in Fran­cis Gu­thrie’s let­ter. By “neigh­bor­ing” coun­tries Gu­thrie must have meant coun­tries ad­ja­cent along a bor­der­line rather than at a single point; oth­er­wise a map whose coun­tries look like the wedges of a pie would re­quire as many col­ors as there are coun­tries. By “coun­try” he cer­tainly must have meant a con­nec­ted re­gion, be­cause if a coun­try is al­lowed to con­sist of more than one re­gion and the re­gions are sep­ar­ate, it is not at all hard to con­struct an ex­ample of a map with five coun­tries each of which is ad­ja­cent to each of the oth­er four [see Fig­ure 1].

Gu­thrie and De Mor­gan cer­tainly real­ized that a map with four coun­tries can be drawn in which each coun­try is ad­ja­cent to the oth­er three [see Fig­ure 2, left]. Such a map re­quires four col­ors and there­fore a three-col­or con­jec­ture is false. Three col­ors will not suf­fice to col­or all maps.

Figure 2. Three colors are not enough to color all maps, as is shown by the map of four countries at the left. Each country is adjacent to the other three, and so the map obviously requires four colors. On the other hand, it is not correct to assume that the number of colors needed to color a map is the same as the highest number of mutually adjacent countries in the map. In the map at the right, for example, no more than three countries are mutually adjacent, and yet four colors are needed: three for outer ring of countries and one for country in the center.

De Mor­gan proved that it is not pos­sible for five coun­tries to be in a po­s­i­tion such that each of them is ad­ja­cent to the oth­er four. This led him to be­lieve that five col­ors would nev­er be needed and thus that the four-col­or con­jec­ture was true. Prov­ing that five mu­tu­ally ad­ja­cent coun­tries can­not ex­ist in a map does not prove the four-col­or con­jec­ture, however [see Fig­ure 2]. Many am­a­teur math­em­aticians, not un­der­stand­ing this fact, have in­de­pend­ently dis­covered proofs of De Mor­gan’s res­ult and have then thought that they had proved the four-col­or con­jec­ture.

In 1878 the math­em­atician Ar­thur Cay­ley, un­able to prove or dis­prove the four-col­or con­jec­ture, presen­ted the prob­lem to the Lon­don Math­em­at­ic­al So­ci­ety. Less than a year later Al­fred Bray Kempe, a bar­ris­ter and mem­ber of the so­ci­ety, pub­lished a pa­per pur­port­ing to show that the con­jec­ture is true. Kempe’s ar­gu­ment was ex­tremely clev­er, and al­though his proof turned out to be in­com­plete, it con­tained most of the ba­sic ideas that led to the cor­rect proof a cen­tury later. Kempe tried to prove the con­jec­ture true by the clas­sic­al meth­od of re­duc­tio ad ab­surdum; he as­sumed that the con­jec­ture is false (that is, that there is at least one map which re­quires five col­ors) and then pro­ceeded to show that this as­sump­tion leads to a con­tra­dic­tion. Reach­ing a con­tra­dic­tion shows that the ori­gin­al as­sump­tion (some maps re­quire five col­ors) is wrong and there­fore the four-col­or con­jec­ture (four col­ors are al­ways enough) is true.

Figure 3. “Normal” maps were defined by Alfred Bray Kempe, who published a faulty proof of the four-color theorem in 1879. A map is normal if no country in it completely surrounds another country or countries and if no more than three countries meet at any point. Map shown here is not normal, since country \( A \) encloses three other countries. Kempe proved correctly that if the four-color theorem could be proved for normal maps, it would be true for all maps, and thus the authors considered only normal maps in their work on theorem.

Kempe began by de­fin­ing nor­mal maps: A map is nor­mal if none of its coun­tries en­close oth­er coun­tries and if no more than three coun­tries meet at any point [see Fig­ure 3]. He then showed that if there were a map that re­quired five col­ors, a “five-chro­mat­ic” map, then there would have to be a nor­mal five-chro­mat­ic map. Thus to prove the four-col­or con­jec­ture it is suf­fi­cient to prove that a nor­mal five-chro­mat­ic map is not pos­sible. Kempe noted that if there were a nor­mal five-chro­mat­ic map, then there would have to be such a map with a smal­lest num­ber of coun­tries, a “min­im­al nor­mal five-chro­mat­ic” map. (In oth­er words, any map with few­er coun­tries than the min­im­al five-chro­mat­ic map can be colored with four or few­er col­ors.) There­fore to prove the four-col­or con­jec­ture it is suf­fi­cient to prove that a min­im­al nor­mal five-chro­mat­ic map is im­possible, that is, that pos­tu­lat­ing the ex­ist­ence of a min­im­al nor­mal map re­quir­ing five col­ors leads to a con­tra­dic­tion.

Figure 4. Map of the easternmost states of the U.S. is normal, but the map of the entire continental U.S. is not: Utah, Colorado, Arizona and New Mexico meet at a single point. (Note that the 48 contiguous states do not even make a proper map because Michigan is made up of two pieces that are not connected.) The maps in Figure 2 are normal, but maps in Figure 1 are not.

Kempe ap­proached a con­tra­dic­tion as fol­lows. He proved that any nor­mal map must have some coun­try with five or few­er neigh­bors. He then ar­gued that if a min­im­al nor­mal five-chro­mat­ic map has a coun­try with few­er than six neigh­bors (which, as he had just shown, every nor­mal map must have), then there would have to be a nor­mal map with few­er coun­tries that is also five-chro­mat­ic. If this ar­gu­ment had been totally cor­rect, a con­tra­dic­tion would have been reached. By as­sum­ing the ex­ist­ence of a min­im­al five-chro­mat­ic map Kempe would have proved the ex­ist­ence of a smal­ler five-chro­mat­ic map. That would con­tra­dict the defin­i­tion of a min­im­al five-chro­mat­ic map, and so no such map would be pos­sible. Since that im­plies that there can be no five-chro­mat­ic map at all, the proof would have been com­plete. Kempe proved cor­rectly that a coun­try with two, three or four neigh­bors ex­ist­ing in a min­im­al five-chro­mat­ic map leads to a con­tra­dic­tion, but his proof of the case of five neigh­bors was faulty. In our proof of the four-col­or the­or­em we cor­rec­ted Kempe’s flawed ana­lys­is of the last case by ex­amin­ing some 1,500 ar­range­ments of coun­tries. Our meth­ods were ba­sic­ally ex­ten­sions of val­id parts of Kempe’s proof that have been the ob­ject of great at­ten­tion and re­fine­ment by math­em­aticians over the past 100 years.

Figure 5. Set of four configurations was proved by Kempe to be “unavoidable,” that is, every normal map includes as a part at least one member of this set. The configurations in the set are a country with two neighbors (a), a country with three neighbors (b), a country with four neighbors (c) and a country with five neighbors (d). Of course, no country can have zero or one neighbor, since neither an island nor an enclosed country is allowed in a normal map.

Kempe had shown that in every nor­mal map there is at least one coun­try with two, three, four or five neigh­bors. (In oth­er words, there are no nor­mal maps on a plane in which every coun­try has six or more neigh­bors.) This may be ex­pressed by the state­ment that the set of “con­fig­ur­a­tions” con­sist­ing of a coun­try with two neigh­bors, a coun­try with three neigh­bors, a coun­try with four neigh­bors and a coun­try with five neigh­bors [see Fig­ure 5] is “un­avoid­able,” that is, every nor­mal map must con­tain at least one of these four con­fig­ur­a­tions. Un­avoid­ab­il­ity is one of the two im­port­ant ideas that are ba­sic to our proof of the four-col­or the­or­em.

The second im­port­ant idea is re­du­cib­il­ity. A con­fig­ur­a­tion is in­tu­it­ively re­du­cible if there is a way of show­ing, solely by ex­amin­ing the con­fig­ur­a­tion and the way in which chains of coun­tries can be aligned, that the con­fig­ur­a­tion can­not pos­sibly ap­pear in a min­im­al five-chro­mat­ic map. Kempe showed that three of his four con­fig­ur­a­tions are re­du­cible but failed to show that a coun­try with five neigh­bors is a re­du­cible con­fig­ur­a­tion. The meth­ods of prov­ing con­fig­ur­a­tions re­du­cible grew out of Kempe’s proof that a coun­try with four neigh­bors can­not oc­cur in a min­im­al five-chro­mat­ic map. The use of the word re­du­cible stems from the form of Kempe’s ar­gu­ment; he proved that if a min­im­al five-chro­mat­ic map con­tains a coun­try with, say, four neigh­bors, then there is a five-chro­mat­ic map with a re­duced num­ber of coun­tries [see Fig­ure 6 and Fig­ure 7].

Figure 6. Kempe showed that to prove the four-color theorem it is sufficient to prove that no minimal five-chromatic map can exist. A minimal five-chromatic map is a map with the fewest countries that requires five colors, that is, any smaller map (any map with fewer countries) can be colored with four colors or fewer. Kempe tried to prove that no minimal five-chromatic map is possible by showing that none of the configurations in his unavoidable set can exist in a minimal five-chromatic map. Each planar map contains one of these configurations, so that if all Kempe’s arguments had been correct, he would have proved the theorem. Kempe’s correct proof that a country, \( D \), with three neighbors (left) cannot be part of a minimal five-chromatic map is as follows. Combine \( D \) with one of its neighbors, \( C \), to form a new country, \( C^{\prime} \) (right). The new map has fewer countries than the original minimal five-chromatic map and so can be colored with four colors. Give all countries of the original map except \( D \) colors they would have in four-coloring of the smaller map. \( D \) can be colored with color not used for \( A \), \( B \) or \( C \). Therefore original map can be colored with four colors: it is not a minimal five-chromatic map. Similar argument shows that no country with two neighbors can be part of minimal five-chromatic map. Proof for country with four neighbors is described in Figure 7.

We can de­scribe Kempe’s at­tack on the four-col­or con­jec­ture as an at­tempt to find an un­avoid­able set of re­du­cible con­fig­ur­a­tions. Find­ing such a set is suf­fi­cient for prov­ing the four-col­or con­jec­ture be­cause it shows that every map con­tains a con­fig­ur­a­tion that can­not be part of a min­im­al five-chro­mat­ic map. There­fore there can be no min­im­al five-chro­mat­ic map, and as Kempe proved cor­rectly this im­plies that there can be no five-chro­mat­ic map at all. Like Kempe, we at­tacked the four-col­or prob­lem by con­struct­ing an un­avoid­able set of re­du­cible con­fig­ur­a­tions. In­stead of four simple con­fig­ur­a­tions, however, our set con­sisted of some 1,500 com­plex fig­ures.

In 1890, 11 years after Kempe pub­lished his proof, Percy John Heawood poin­ted out that Kempe’s ar­gu­ment that no min­im­al five-chro­mat­ic map could con­tain a coun­try with five neigh­bors was flawed, and that the er­ror did not ap­pear easy to re­pair. In his at­tack on the prob­lem Heawood in­vest­ig­ated a gen­er­al­iz­a­tion of the ori­gin­al four-col­or con­jec­ture. The maps stud­ied by Gu­thrie and Kempe were maps in a plane or on a sphere. Heawood, con­sid­er­ing maps on more com­plic­ated sur­faces, was able to ob­tain an el­eg­ant ar­gu­ment that provided an up­per bound for the num­ber of col­ors re­quired to col­or maps on these sur­faces. If the meth­od he used had been ap­plic­able to the plane, it would have provided a proof of the four-col­or con­jec­ture.

Figure 7. Reducible configuration is an arrangement of countries that cannot be part of a minimal five-chromatic map. To prove the four-color theorem Kempe tried to show that the four configurations in his unavoidable set are reducible. He failed because he could not prove that a country with five neighbors is a reducible configuration. The authors succeeded in proving the theorem by producing an unavoidable set of some 1,500 reducible configurations. The concept of reducibility is derived from Kempe’s correct proof that a country with four neighbors, say \( E \), cannot be part of a minimal five-chromatic map. As in the case of a country with three neighbors (see Figure 6), \( E \) can be combined with a neighbor to establish a four-coloring for all the other countries in the map (top). If the four neighbors of \( E \) are colored with fewer than four colors, an unused color can be assigned to \( E \) to show that the map is four-colorable. Otherwise consider the colors of a pair of countries on opposite sides of \( E \). Either there is a path of countries colored with these two colors leading from one country to the other or there is no such path. In this example \( A \) and \( C \) are connected by a path of dark-color and dark-gray countries, but no path of light-gray and light-color countries connects \( B \) and \( D \). A theorem states that if both pairs of countries are joined by such paths, then the paths have a country in common. This is clearly impossible, since the common country would have to be colored with two distinct colors. Therefore at least one pair of countries (here \( B \) and \( D \)) will not be linked by a path of countries the colors of the pair. The light-gray and light-color countries that form a path from \( B \) are \( U \), \( V \), \( W \) and \( X \). Reverse colors of the countries in this group. In this case make the light-gray countries light color and the light-color countries light gray (bottom). Now uncolored country has neighbors colored with only three colors, so that it can be given the fourth color (light gray here) to produce a four-coloring for the minimal five-chromatic map. In other words, a country with four neighbors cannot be part of a minimal five-chromatic map.

Heawood con­tin­ued to work on the prob­lem for no less than 60 years. Dur­ing that time many oth­er em­in­ent math­em­aticians de­voted a great deal of ef­fort to the four-col­or con­jec­ture. One may won­der why so many math­em­aticians would spend so much time on what ap­peared to be a ques­tion of so little prac­tic­al sig­ni­fic­ance. The ex­plan­a­tion lies in the dis­cov­er­ies made about the nature of pure math­em­at­ics over the past cen­tury and in the ef­fect of those dis­cov­er­ies on the faith of math­em­aticians in the power of math­em­at­ics.

To­ward the end of the 19th cen­tury math­em­aticians were able to build power­ful the­or­ies that en­abled them to settle many dif­fi­cult ques­tions. The feel­ing grew that any ques­tion that could be reas­on­ably posed in the lan­guage of math­em­at­ics could be answered by the use of suf­fi­ciently power­ful math­em­at­ic­al ideas. Moreover, it was be­lieved that these ques­tions could be answered in such a way that a com­pet­ent math­em­atician could check the cor­rect­ness of the an­swer in a reas­on­able length of time. The four-col­or con­jec­ture cer­tainly ap­peared to be such a prob­lem. If math­em­aticians could not solve the prob­lem, it seemed clear that they had simply not yet de­veloped the ap­pro­pri­ate math­em­at­ic­al tools.

In the 1930’s, however, new dis­cov­er­ies chal­lenged the 19th-cen­tury faith in the com­plete­ness of math­em­at­ics. Kurt Gödel and Alonzo Church ob­tained new and dis­turb­ing res­ults in form­al lo­gic, the branch of math­em­at­ics in which the concept of proof is stated most pre­cisely. It was proved that in what seems to be the most nat­ur­al lo­gic­al sys­tem there are true state­ments that can­not be proved true (or false) in the sys­tem. Moreover, there are the­or­ems in the sys­tem with re­l­at­ively short state­ments whose shortest proofs are too long to be writ­ten down in any reas­on­able length of time. In the 1950’s fur­ther in­vest­ig­a­tion showed that the same dif­fi­culties af­fect branches of math­em­at­ics oth­er than lo­gic. Some math­em­aticians began to think that the four-col­or con­jec­ture might be one of those state­ments that can neither be proved nor dis­proved; after all, the con­jec­ture had been stud­ied without suc­cess for 80 years. Oth­er work­ers felt that if a proof ex­is­ted, it would be too long to write down. Many be­lieved, however, that the dis­ease of un­solv­ab­il­ity could not spread to this area of math­em­at­ics and that an el­eg­ant math­em­at­ic­al ar­gu­ment would be found to de­cide the truth or false­hood of the four-col­or con­jec­ture.

We now know that a proof can be found. But we do not yet know (and may nev­er know) wheth­er there is any proof that is el­eg­ant, con­cise and com­pletely com­pre­hens­ible by a hu­man math­em­at­ic­al mind. So many areas of math­em­at­ics have been in­volved in vari­ous at­tempts to prove the four-col­or con­jec­ture that it would be im­possible to dis­cuss them all here. We shall re­strict our at­ten­tion to work that led dir­ectly to the proof.

In 1913 George D. Birk­hoff of Har­vard Uni­versity im­proved on Kempe’s re­duc­tion tech­nique and was able to show that cer­tain con­fig­ur­a­tions lar­ger than Kempe’s were re­du­cible. Philip Frank­lin of the Mas­sachu­setts In­sti­tute of Tech­no­logy util­ized some of Birk­hoff’s res­ults to show that a map re­quir­ing five col­ors must have at least 22 coun­tries, that is, that any map with few­er than 22 coun­tries is four-col­or­able. Birk­hoff’s meth­ods were im­proved by many math­em­aticians between 1913 and 1950. Dur­ing this peri­od re­du­cible con­fig­ur­a­tions were ex­ploited primar­ily to im­prove Frank­lin’s res­ult; by 1950 it had been shown that any map with few­er than 36 coun­tries is four-col­or­able.

Al­though the work in this area did show that many con­fig­ur­a­tions are re­du­cible, the set of all the con­fig­ur­a­tions that had been proved re­du­cible by 1950 did not even come close to form­ing an un­avoid­able set. Only a few math­em­aticians had con­struc­ted un­avoid­able sets of con­fig­ur­a­tions, and there was little hope that their work would lead to an un­avoid­able set of re­du­cible con­fig­ur­a­tions.

Hein­rich Heesch of the Uni­versity of Han­nov­er seems to have been the first math­em­atician after Kempe to pub­licly state that the four-col­or con­jec­ture could be proved by find­ing an un­avoid­able set of re­du­cible con­fig­ur­a­tions. Heesch, who began his work on the con­jec­ture in 1936, made sev­er­al ma­jor con­tri­bu­tions to the ex­ist­ing the­ory. In 1950 he es­tim­ated that the re­du­cible con­fig­ur­a­tions in the (then) hy­po­thet­ic­al un­avoid­able set would be of cer­tain re­stric­ted sizes and num­ber about 10,000.

Con­fig­ur­a­tion size must be a ma­jor con­sid­er­a­tion in this ap­proach to the four-col­or prob­lem. In the cen­tury since Kempe first in­tro­duced the idea of re­du­cib­il­ity cer­tain stand­ard meth­ods for ex­amin­ing con­fig­ur­a­tions to de­term­ine wheth­er or not they are re­du­cible have been de­veloped. Em­ploy­ing these meth­ods to show that large con­fig­ur­a­tions are re­du­cible re­quires the ex­am­in­a­tion of a large num­ber of de­tails and ap­pears feas­ible only by com­puter. Every con­fig­ur­a­tion is sur­roun­ded by a ring of neigh­bors; the ring size, or num­ber of coun­tries that form the ring around the con­fig­ur­a­tion, has a dir­ect bear­ing on the dif­fi­culty of prov­ing the con­fig­ur­a­tion re­du­cible. When one is try­ing to con­struct an un­avoid­able set of re­du­cible con­fig­ur­a­tions and dis­cov­ers that a par­tic­u­lar con­fig­ur­a­tion is not re­du­cible, one can of­ten re­place it to good ef­fect with one or more oth­er con­fig­ur­a­tions, usu­ally con­fig­ur­a­tions of a lar­ger ring size. Re­pla­cing one con­fig­ur­a­tion with an­oth­er whose ring con­tains an ad­di­tion­al ver­tex, however, greatly in­creases the dif­fi­culty of re­du­cib­il­ity test­ing and the com­puter time needed for it. This is in part be­cause the num­ber of dis­tinct prop­er col­or­ings of the ver­tices of the new ring is about three times the num­ber of col­or­ings of the ver­tices in the ori­gin­al ring. Fur­ther­more, pro­grams to test re­du­cib­il­ity con­sider each pos­sible col­or­ing sev­er­al times. In 1950 the dif­fi­culties of com­pu­ta­tion seemed to rule out the pos­sib­il­ity of pro­du­cing an un­avoid­able set of con­fig­ur­a­tions and prov­ing that each of its mem­bers is re­du­cible.

With the ad­vent of high-speed di­git­al com­puters, however, an at­tack on these prob­lems be­came tech­nic­ally pos­sible. Heesch form­al­ized the known meth­ods of prov­ing con­fig­ur­a­tions re­du­cible and ob­served that at least one of them (a straight­for­ward gen­er­al­iz­a­tion of the meth­od used by Kempe) was in prin­ciple a suf­fi­ciently mech­an­ic­al pro­ced­ure to be im­ple­men­ted by com­puter. Heesch’s stu­dent Karl Dürre then wrote a com­puter pro­gram that used this pro­ced­ure to prove con­fig­ur­a­tions re­du­cible. Whenev­er such a pro­gram suc­ceeds in prov­ing a con­fig­ur­a­tion re­du­cible, the con­fig­ur­a­tion is cer­tainly re­du­cible. A neg­at­ive res­ult, however, shows only that the par­tic­u­lar meth­od of prov­ing re­du­cib­il­ity is not suf­fi­cient to prove the con­fig­ur­a­tion re­du­cible; it might be pos­sible to prove it re­du­cible by oth­er meth­ods. In some cases, when Dürre’s pro­gram failed to prove a con­fig­ur­a­tion re­du­cible, Heesch suc­ceeded. He was able to show the con­fig­ur­a­tions re­du­cible with data gen­er­ated by the pro­gram and with fur­ther cal­cu­la­tions us­ing a stronger tech­nique de­veloped by Birk­hoff.

Figure 8. A dual graph (color) displays the countries and borders of the original map (left). The dual graph is constructed by marking a vertex in each country of the original map and then connecting the vertices of each pair of neighboring countries with an edge across their common border. These edges can always be drawn as straight lines, so that they divide the plane into polygonal faces. When the original map is normal, these faces are triangles and the graph is called a triangulation of the plane. The number of edges meeting at a vertex is called the degree of the vertex and is equal to the number of neighbors of the country (in the original map) represented by that vertex.

Heesch de­scribed con­fig­ur­a­tions in a con­veni­ent way. He began by trans­form­ing the ori­gin­al map in­to what math­em­aticians call a dual form: a planar graph in which each ver­tex of the graph rep­res­ents a coun­try and each line seg­ment between ver­tices rep­res­ents a bor­der. To ob­tain a dual graph of a map mark the cap­it­al in each coun­try in the map and then, whenev­er two coun­tries are neigh­bors, join their cap­it­als by a road across the com­mon bor­der [see Fig­ure 8]. Now re­move everything ex­cept the cap­it­als (called ver­tices) and the roads (called edges) you have ad­ded. These ver­tices and edges form the dual graph of the ori­gin­al map. The edges of a graph di­vide the plane in­to re­gions that are called faces. If the ori­gin­al map is nor­mal (and only nor­mal maps must be con­sidered in the proof of the four-col­or the­or­em), all of the faces are tri­angles. In this case the dual graph is called a tri­an­gu­la­tion. The num­ber of edges that end at a par­tic­u­lar ver­tex (in the dual graph) is called the de­gree of the ver­tex and is equal to the num­ber of neigh­bors of the coun­try (in the ori­gin­al map) that is rep­res­en­ted by that ver­tex. A path of edges that starts and ends at the same ver­tex and does not cross it­self sep­ar­ates the graph in­to two parts: its in­teri­or and its ex­ter­i­or. Such a path is called a cir­cuit.

In the vocab­u­lary of dual graphs a con­fig­ur­a­tion is a part of a tri­an­gu­la­tion con­sist­ing of a set of ver­tices plus all of the edges join­ing them. The bound­ary cir­cuit, con­sist­ing of those ver­tices ad­ja­cent to the con­fig­ur­a­tion and the edges join­ing them, is called the ring of the con­fig­ur­a­tion. (The ring in the graph cor­res­ponds to the ring of coun­tries that bound the con­fig­ur­a­tion in the ori­gin­al map.) Con­fig­ur­a­tions are of­ten de­scribed by the lengths of their rings: a six-ring con­fig­ur­a­tion, for ex­ample, is one whose bound­ary cir­cuit has ex­actly six ver­tices.

With Heesch’s work the the­ory of re­du­cible con­fig­ur­a­tions seemed ex­tremely well de­veloped. Al­though cer­tain im­prove­ments in the meth­ods of prov­ing re­du­cib­il­ity have since been made, all of the ideas on re­du­cib­il­ity that were needed for the proof of the four-col­or the­or­em were un­der­stood in the late 1960’s. Com­par­able pro­gress had not been made in find­ing un­avoid­able sets of con­fig­ur­a­tions. Heesch in­tro­duced a meth­od that was ana­log­ous to mov­ing charge in an elec­tric­al net­work to find an un­avoid­able set of con­fig­ur­a­tions (not ne­ces­sar­ily re­du­cible), but he had not treated the idea of un­avoid­ab­il­ity with the same en­thu­si­asm as the idea of re­du­cib­il­ity. This meth­od of “dis­char­ging” that first ap­peared in rather rudi­ment­ary form in the work of Heesch has been cru­cial, however, in all later work on un­avoid­able sets. In a much more soph­ist­ic­ated form it be­came the cent­ral ele­ment in the proof of the four-col­or the­or­em; hence we will ex­plain it in some de­tail.

Kempe’s work shows that a tri­an­gu­la­tion that rep­res­ents a min­im­al five-chro­mat­ic map can­not have any ver­tices with few­er than five neigh­bors. Thus in what fol­lows we will for con­veni­ence use the word tri­an­gu­la­tion to mean a tri­an­gu­la­tion with no ver­tices of de­gree less than five. If we as­sign the charge num­ber 6-\( k \) to every ver­tex of de­gree \( k \) (that is, with \( k \) neigh­bors), then ver­tices of de­gree great­er than six (ma­jor ver­tices) are as­signed neg­at­ive charge and only ver­tices of de­gree five are giv­en pos­it­ive charge. It fol­lows from Kempe’s work that the sum of the as­signed num­bers of any tri­an­gu­la­tion is ex­actly 12. This some­what sur­pris­ing res­ult de­pends both on the fact that the graph is drawn in the plane and that it is a tri­an­gu­la­tion. The par­tic­u­lar sum of 12 is not very im­port­ant. What is ex­tremely im­port­ant is that for every planar tri­an­gu­la­tion this charge sum is pos­it­ive.

Now sup­pose the charges in such a tri­an­gu­la­tion are re­dis­trib­uted, moved around without los­ing or gain­ing charge in the en­tire sys­tem. In par­tic­u­lar sup­pose pos­it­ive charge is moved from some of the pos­it­ively charged (de­gree-five) ver­tices to some of the neg­at­ively charged (ma­jor) ver­tices. It is cer­tainly not pos­sible to change the (pos­it­ive) sum of the charges by these op­er­a­tions, but the ver­tices hav­ing pos­it­ive charge may change; for ex­ample, some de­gree-five ver­tices may lose all pos­it­ive charge (be­come dis­charged), where­as some ma­jor ver­tices may gain so much charge that they end up with pos­it­ive charge (be­come over­charged). Dif­fer­ent ver­tices be­come dis­charged or over­charged ac­cord­ing to the dis­char­ging, or re­dis­tri­bu­tion, pro­ced­ure chosen.

Giv­en a spe­cified dis­char­ging pro­ced­ure on an ar­bit­rary graph, however, it is pos­sible to make a fi­nite list of all the con­fig­ur­a­tions that, after dis­char­ging is done, have ver­tices of pos­it­ive charge.

(Of course, each of these con­fig­ur­a­tions can be re­peated an un­fore­see­able num­ber of times.) In oth­er words, pos­it­ive charge can only oc­cur with­in this fi­nite set of con­fig­ur­a­tions. Since the total charge is al­ways pos­it­ive, there will al­ways be some ver­tices of pos­it­ive charge. There­fore since all pos­sible re­cept­acles of pos­it­ive charge are in­cluded in the list of con­fig­ur­a­tions, every planar tri­an­gu­la­tion must con­tain at least one of these con­fig­ur­a­tions. This pro­cess — gen­er­at­ing a list of spe­cif­ic con­fig­ur­a­tions from an ar­bit­rary map — works be­cause it is pos­sible to de­term­ine the lay­out of small pieces of the map without know­ing the form of the com­plete map.

In the proof of the four-col­or the­or­em the pur­pose of this dis­char­ging of pos­it­ive ver­tices is to find a pro­ced­ure de­scrib­ing ex­actly how to move charge in such a way as to en­sure that every ver­tex of pos­it­ive charge in the res­ult­ing con­fig­ur­a­tion must either be­long to a re­du­cible con­fig­ur­a­tion or be ad­ja­cent to one. Since the con­fig­ur­a­tions signaled by this pro­ced­ure must form an un­avoid­able set, if they are also re­du­cible, then the four-col­or con­jec­ture is proved. Of course, if not all of the res­ult­ing con­fig­ur­a­tions are re­du­cible, then no real pro­gress has been made. In fact. Kempe’s un­avoid­able set can be con­sidered to be the one res­ult­ing from the in­ef­fect­ive pro­ced­ure of mov­ing no charges at all.

Figure 9. Discharging procedure generates an unavoidable set of reducible configurations by redistributing the positive charge of an arbitrary triangulation (with no vertices of degree less than five) so that positive charge occurs only in reducible configurations. Since there is positive charge in every map, an unavoidable set can be formed by choosing configurations occurring in every type of neighborhood of positive charge. If each configuration in the set is reducible, then there can be no minimal five-chromatic map and the four-color theorem is proved. An example of a simple discharging procedure is the transfer of 1/5 unit of charge from each positively charged vertex to each of its negatively charged neighbors. In this process a degree-five vertex (black circles) ends with positive charge only if it has (a) a degree-five neighbor or (b) a degree-six neighbor (gray circles), so that it is forced to retain charge. A degree-six vertex never becomes positive because, having an initial charge of zero, it never receives positive charge. A degree-seven vertex finishes with positive charge only if it has at least six degree-five neighbors; then at least two of them will be adjacent (a). Vertices of degree greater than seven can never receive enough positive charge to overcome their initial negative charge. The unavoidable set generated by this discharging procedure consists of a degree-five vertex joined by an edge to another degree-five vertex (a) and a degree-five vertex joined by an edge to a degree-six vertex (b). These configurations are not reducible. If procedure is modified to transfer 1/3 unit of charge from each positively charged vertex to each of its negatively charged neighbors, slightly better set (c, d) is generated. If 1/2 unit of charge is transferred, resulting set is close to one produced by early version of authors’ discharging procedure.

An ex­ample of a rather simple dis­char­ging pro­ced­ure and the as­so­ci­ated un­avoid­able set may make these ideas clear­er. Con­sider the pro­ced­ure that trans­fers 1/5 unit of charge from every de­gree-five ver­tex to each of its ma­jor neigh­bors [see Fig­ure 9]. The cor­res­pond­ing un­avoid­able set con­sists of two con­fig­ur­a­tions. One is a pair of de­gree-five ver­tices joined by an edge and the oth­er is a de­gree-five ver­tex joined by an edge to a de­gree-six ver­tex.

These con­fig­ur­a­tions are ob­tained as fol­lows. A de­gree-five ver­tex can only end up pos­it­ive in this pro­ced­ure if at least one of its neigh­bors is not ma­jor, so that the ver­tex is forced to re­tain pos­it­ive charge; the ver­tex either has a de­gree-five neigh­bor (the situ­ation cor­res­pond­ing to the first con­fig­ur­a­tion in the set) or a de­gree-six neigh­bor (the second con­fig­ur­a­tion).

A de­gree-six ver­tex starts with no charge and there­fore can­not re­ceive any. A de­gree-sev­en ver­tex can only be­come pos­it­ive if it has at least six neigh­bors that are de­gree-five ver­tices; if it has at least six such neigh­bors, two of them are joined by an edge (the first con­fig­ur­a­tion of the un­avoid­able set). A ver­tex of de­gree eight or high­er can­not be­come pos­it­ive even if all of its neigh­bors are de­gree-five ver­tices. This can be seen by ex­amin­ing a de­gree-eight ver­tex. Its charge is minus two and the max­im­um pos­it­ive charge it can re­ceive is eight times 1/5, or 1 3/5. Thus the two (nonre­du­cible) con­fig­ur­a­tions form an un­avoid­able set; that is, since these cal­cu­la­tions ap­ply to any planar tri­an­gu­la­tion (with no ver­tices of de­gree less than five) a mem­ber of the two-con­fig­ur­a­tion set will be found in every such tri­an­gu­la­tion of the plane.

In 1970 one of us (Haken) no­ticed cer­tain meth­ods of im­prov­ing dis­char­ging pro­ced­ures and began to hope that such im­prove­ments might lead to a proof of the four-col­or con­jec­ture. The dif­fi­culties, however, still ap­peared to be for­mid­able. One was that it was be­lieved that very large con­fig­ur­a­tions (with rings of neigh­bors con­tain­ing as many as 18 ver­tices) would be in­cluded in any un­avoid­able set of re­du­cible con­fig­ur­a­tions. This meant that the prob­lem might be bey­ond the cap­ab­il­it­ies of ex­ist­ing com­puters be­cause al­though test­ing con­fig­ur­a­tions of small ring size (up to about 11 ver­tices) for re­du­cib­il­ity was reas­on­ably simple on a com­puter, the com­puter time re­quired in­creased by a factor of four for every unit in­crease in ring size. To make things worse, the com­puter stor­age re­quire­ments in­creased just as quickly. When Dürre’s pro­gram was ap­plied to a par­tic­u­larly dif­fi­cult 14-ring con­fig­ur­a­tion, it took 26 hours to prove that the con­fig­ur­a­tion did not sat­is­fy even the most mech­an­ic­al defin­i­tion of re­du­cib­il­ity (the defin­i­tion stated with the few­est ma­chine in­struc­tions). Even if the av­er­age time re­quired to ex­am­ine a 14-ring con­fig­ur­a­tion were only 25 minutes, test­ing an av­er­age 18-ring con­fig­ur­a­tion would re­quire \( 4^4 \times 25 \) minutes, or more than 100 hours, of com­puter time and more stor­age than was avail­able on any ex­ist­ing com­puter.

An­oth­er ma­jor dif­fi­culty was that no one really knew how many re­du­cible con­fig­ur­a­tions would be needed to form an un­avoid­able set. It seemed likely that the num­ber of con­fig­ur­a­tions would be in the thou­sands, but no up­per lim­it had been es­tab­lished. Sup­pose that on a com­puter with suf­fi­cient stor­age it takes 100 hours to show that an 18-ring con­fig­ur­a­tion is re­du­cible. If there are 1,000 18-ring con­fig­ur­a­tions in the set, it would take 100,000 hours, or more than 11 years, to prove them re­du­cible on a very large com­puter. For all prac­tic­al pur­poses if the set had been that large, the proof would have had to wait for com­puters much faster than those cur­rently avail­able.

Even if the the­or­em could be proved by find­ing an un­avoid­able set of re­du­cible con­fig­ur­a­tions, the proof would not sat­is­fy those who de­mand math­em­at­ic­al el­eg­ance. What would be even more up­set­ting to many math­em­aticians, no one would be able to check the re­du­cib­il­ity of all the con­fig­ur­a­tions in the set by hand. By 1970, however, many ex­perts on the four-col­or prob­lem were quite pess­im­ist­ic about find­ing a short proof. The prob­lem had re­ceived a great deal of at­ten­tion since its for­mu­la­tion more than 100 years earli­er. Many ap­proaches to the prob­lem had been tried, but al­though some had led to im­port­ant res­ults in oth­er areas of math­em­at­ics, none had ever led to a proof of the four-col­or the­or­em.

When we began our work on the prob­lem in 1972, we felt cer­tain that the tech­niques avail­able to us would not lead to a non­com­puter proof. We were even quite doubt­ful that they could lead to any proof at all be­fore much more power­ful com­puters were de­veloped. There­fore our first step in at­tack­ing the prob­lem of find­ing an un­avoid­able set of re­du­cible con­fig­ur­a­tions was to de­term­ine wheth­er or not there was any hope of find­ing such a set with con­fig­ur­a­tions of ring size suf­fi­ciently small that the com­puter time for the proofs of re­du­cib­il­ity would be with­in reas­on. By the very nature of this ques­tion it was clear that we should not be­gin by ex­amin­ing the re­du­cib­il­ity of all the con­fig­ur­a­tions con­sidered; oth­er­wise the time spent in mak­ing the es­tim­ate would ex­ceed the ex­pec­ted time needed for the en­tire task.

Here a thought of Heesch’s proved ex­tremely use­ful. While he was test­ing con­fig­ur­a­tions for re­du­cib­il­ity he ob­served a num­ber of dis­tinct­ive phe­nom­ena that provide clues to the like­li­hood of suc­cess­ful re­duc­tion. For ex­ample, there are cer­tain con­di­tions in­volving the neigh­bors of ver­tices of a con­fig­ur­a­tion un­der which no re­du­cible con­fig­ur­a­tion had ever been found. No re­du­cible con­fig­ur­a­tion had ever been found that con­tained, for in­stance, at least two ver­tices, a ver­tex ad­ja­cent to four ver­tices of the ring and no smal­ler re­du­cible con­fig­ur­a­tions. Al­though no proof is known that re­du­cible con­fig­ur­a­tions with these re­duc­tion obstacles could not ex­ist, it seemed prudent to as­sume that if one wanted re­du­cible con­fig­ur­a­tions, one should avoid such con­fig­ur­a­tions. Heesch found three ma­jor re­duc­tion obstacles, in­clud­ing the one de­scribed above, that could be eas­ily de­scribed [see Fig­ure 10]. No con­fig­ur­a­tion con­tain­ing one of them has ever been proved to be re­du­cible.

Figure 10. Three reduction obstacles were observed by Heinrich Heesch of the University of Hannover. These arrangements of vertices seem to occur only in configurations that cannot be proved reducible. Thus the authors could use the obstacles to identify potential problem areas in their proof. In the graphs shown here the configurations are the arrangements of vertices joined by heavy solid lines. Thinner solid lines connect the vertices of the ring, or outer boundary, of the configuration. Broken lines connect configuration vertices to ring vertices. Each configuration contains one of Heesch’s reduction obstacles: vertex \( V \) (left) has four neighbors on the ring of the configuration; vertex \( W \) (middle) has three nonconsecutive neighbors on the ring of the configuration; vertices \( X \) and \( Y \) (right) form what is called a hanging pair, that is, these vertices are joined to each other and to ring vertices but have only one other neighbor in the configuration.

It is easy to de­term­ine wheth­er or not a con­fig­ur­a­tion con­tains a re­duc­tion obstacle, and con­fig­ur­a­tions without re­duc­tion obstacles have a very good chance of be­ing re­du­cible. If there was a man­age­able un­avoid­able set of con­fig­ur­a­tions free of re­duc­tion obstacles, we felt there would have to be an un­avoid­able set of roughly the same size con­tain­ing only re­du­cible con­fig­ur­a­tions.

We there­fore de­cided to first study cer­tain kinds of dis­char­ging pro­ced­ure in or­der to de­term­ine the types of sets of obstacle-free con­fig­ur­a­tions that might arise. To gain an un­der­stand­ing of what was needed, even for this study, we re­stric­ted the already re­stric­ted prob­lem to what are called geo­graph­ic­ally good con­fig­ur­a­tions: con­fig­ur­a­tions that do not con­tain the first two of Heesch’s three obstacles.

In the fall of 1972 we wrote a com­puter pro­gram that would carry out the par­tic­u­lar type of dis­char­ging pro­ced­ure that seemed most reas­on­able to us. We were not ready to prove the the­or­em, so that the out­put of our pro­gram was not an un­avoid­able set but rather a list of the con­fig­ur­a­tions that res­ul­ted from the most im­port­ant situ­ations. Al­though a com­puter pro­gram could not be ex­pec­ted to pro­ceed as clev­erly as a hu­man be­ing, the im­mense speed of the com­puter made it pos­sible to ac­cept cer­tain in­ef­fi­cien­cies. In any event the pro­gram was writ­ten in such a way that its out­put could be eas­ily checked by hand.

Figure 11. Example of a planar triangulation includes one degree-eight vertex (gray square), one degree-seven vertex (large gray circle), eight degree-six vertices (small gray circles) and 15 degree-five vertices (small black circles). Kempe proved that vertices of degree two, three and four are reducible, that is, they cannot occur in a minimal five-chromatic map. Therefore in order to disprove the existence of a minimal five-chromatic map the authors needed to consider only those triangulations with vertices of degree five or more. The “charge” (numerals in color) of a vertex is defined as six minus the degree of that vertex. Since the triangulations under consideration have no vertices of degree four or less, the only vertices with positive charge are those of degree five. It is not difficult to prove that the total charge in any normal map equals 12. This fact implies that there will be positively charged (that is, degree-five) vertices in every triangulation of the plane involved in the proof of four-color theorem.

The first runs of the com­puter pro­gram in late 1972 gave us a great deal of valu­able in­form­a­tion. First, it ap­peared that geo­graph­ic­ally good con­fig­ur­a­tions of reas­on­able size (with a ring size of no more than 16) would be found close to most ver­tices of ul­ti­mately pos­it­ive charge. Second, the same con­fig­ur­a­tions oc­curred fre­quently enough for it to ap­pear that the list of con­fig­ur­a­tions might be of man­age­able length. Third, as the pro­ced­ure was ori­gin­ally or­gan­ized the com­puter out­put was too large to handle; sim­il­ar cases re­peated the same ar­gu­ment too of­ten. Fourth, there were clearly some flaws in the pro­ced­ure, since there were ver­tices of ul­ti­mately pos­it­ive charge in whose neigh­bor­hoods no geo­graph­ic­ally good con­fig­ur­a­tions could be guar­an­teed. Fi­nally, the pro­gram gen­er­ated a tre­mend­ous amount of in­form­a­tion in only a few hours of com­puter time, so that we knew it would be pos­sible to ex­per­i­ment of­ten.

The pro­gram and cer­tain as­pects of the dis­char­ging pro­ced­ure had to be mod­i­fied to over­come the prob­lems in­dic­ated by the first com­puter runs. Since we could pre­serve the ba­sic pro­gram struc­ture, the changes were not too dif­fi­cult to make, and a month later we made a second set of runs. Now that the ma­jor prob­lems had been cor­rec­ted, we could per­ceive subtler prob­lems. After some study we found solu­tions to these prob­lems and again mod­i­fied the pro­gram.

The man-ma­chine dia­logue con­tin­ued for an­oth­er six months un­til we felt that our pro­ced­ure would ob­tain an un­avoid­able set of geo­graph­ic­ally good con­fig­ur­a­tions in a reas­on­able amount of time. At this point we de­cided to prove form­ally that the pro­ced­ure would provide a fi­nite un­avoid­able set of geo­graph­ic­ally good con­fig­ur­a­tions. We had to put aside the ex­per­i­ment­al ap­proach and de­scribe the total pro­ced­ure. It was ne­ces­sary to prove that all cases had been covered and that those cases that were not handled by the com­puter pro­gram were as simple as they ap­peared to be.

Much to our sur­prise this task proved ex­tremely dif­fi­cult and took more than a year. It was ne­ces­sary to for­mu­late gen­er­al defin­i­tions of terms and to prove ab­stract state­ments about them. Spe­cial cases, even those that were not likely to arise in prac­tice, had to be ex­amined in de­tail and of­ten re­quired com­plic­ated ana­lyses. Fi­nally, by the fall of 1974, we had a lengthy proof that a fi­nite un­avoid­able set of geo­graph­ic­ally good con­fig­ur­a­tions does ex­ist, and we had a pro­ced­ure for con­struct­ing such a set with pre­cise, al­though much lar­ger than de­sir­able, bounds on the size of the con­fig­ur­a­tions in the set. The pro­ced­ure we had de­signed was ex­tremely im­port­ant to us be­cause we in­ten­ded to ap­ply it in the proof of the four-col­or the­or­em. (A short time later Wal­ter Strom­quist, a ma­jor con­trib­ut­or to re­duc­tion the­ory who was then a gradu­ate stu­dent at Har­vard, de­vised an el­eg­ant proof of the ex­ist­ence of un­avoid­able sets of geo­graph­ic­ally good con­fig­ur­a­tions. Since Strom­quist’s proof did not provide a meth­od of ac­tu­ally con­struct­ing the con­fig­ur­a­tions in the set, however, it ap­peared un­likely that it would be im­me­di­ately ap­plic­able to the four-col­or con­jec­ture it­self.)

When we had proved that our pro­ced­ure would work for geo­graph­ic­ally good con­fig­ur­a­tions, we still did not know how com­plic­ated car­ry­ing out the pro­ced­ure would be. We de­cided to try it on the re­stric­ted prob­lem of tri­an­gu­la­tions hav­ing no pairs of ad­ja­cent de­gree-five ver­tices. This, of course, is a strong re­stric­tion, but the un­avoid­able set of geo­graph­ic­ally good con­fig­ur­a­tions we ob­tained was quite small: only 47 con­fig­ur­a­tions and none of them of a ring size lar­ger than 16. We guessed that the solu­tion to the un­res­tric­ted prob­lem might be 50 times more un­wieldy (this turned out to be a bit op­tim­ist­ic), and we de­cided that there was good reas­on to con­tin­ue. Early in 1975 we mod­i­fied the pro­gram so that it pro­duced obstacle-free con­fig­ur­a­tions rather than geo­graph­ic­ally good ones and forced it to search for sets in which more of the con­fig­ur­a­tions had small ring size. When we ran the mod­i­fied pro­gram, cer­tain flaws be­came evid­ent but there was also a very pleas­ant sur­prise: Re­pla­cing geo­graph­ic­ally good con­fig­ur­a­tions with obstacle-free ones only doubled the size of the un­avoid­able set.

At this point the pro­gram, which had been ab­sorb­ing our ideas and im­prove­ments for two years, began to sur­prise us. When we had hand-checked the ana­lyses pro­duced by the early ver­sions of the pro­gram, we were al­ways able to pre­dict their course, but now the com­puter was act­ing like a chess-play­ing ma­chine. It was work­ing out com­pound strategies based on all the tricks it had been taught, and the new ap­proaches were of­ten much cleverer than those we would have tried. In a sense the pro­gram was demon­strat­ing su­peri­or­ity not only in the mech­an­ic­al parts of the task but in some in­tel­lec­tu­al areas as well.

By the sum­mer of 1975 we be­lieved that there was a good chance that we could find an un­avoid­able set of con­fig­ur­a­tions each of which would be obstacle-free and likely to be re­du­cible. Such a set would cer­tainly con­tain some ir­re­du­cible con­fig­ur­a­tions, but we felt that by some small change of pro­ced­ure we would be able to re­place them with re­du­cible con­fig­ur­a­tions. Now for the first time we would have to test con­fig­ur­a­tions for re­du­cib­il­ity.

We began by writ­ing a pro­gram to test for the most mech­an­ic­al re­du­cib­il­ity, work­ing with the as­sem­bler lan­guage for the Uni­versity of Illinois IBM 360 com­puter. We had been joined the pre­ced­ing fall by John Koch, a gradu­ate stu­dent in com­puter sci­ence who chose to write a dis­ser­ta­tion on the re­du­cib­il­ity of con­fig­ur­a­tions of small ring size. (Frank Al­laire of the Uni­versity of Man­itoba and Ed­ward Swart of the Uni­versity of Rhodesia were do­ing some­what sim­il­ar work of which we were un­aware.) By the fall of 1975 Koch had writ­ten pro­grams to check for the most mech­an­ic­al re­du­cib­il­ity in con­fig­ur­a­tions of a ring size up to 11 and had gone on to more gen­er­al in­vest­ig­a­tions.

Over the next few months, with Koch’s aid, we mod­i­fied his work on 11-ring con­fig­ur­a­tions to pro­duce pro­grams for check­ing the re­du­cib­il­ity of 12-, 13- and 14-ring con­fig­ur­a­tions. Fi­nally we fur­ther mod­i­fied these pro­grams to ap­ply a more gen­er­al pro­ced­ure for re­duc­tion that had been de­veloped by Birk­hoff.

At this point our work on the dis­char­ging pro­ced­ure reached an im­passe. Struc­tur­al changes, not just ad­just­ments of para­met­ers and small ad­di­tions, were re­quired to im­prove the pro­gram, and each change would mean a ma­jor modi­fic­a­tion of it. We there­fore de­cided to dis­card the pro­gram and im­ple­ment the dis­char­ging pro­ced­ure by hand. This would en­sure great­er flex­ib­il­ity and al­low the pro­ced­ure to be mod­i­fied loc­ally whenev­er ne­ces­sary. In Decem­ber, 1975, we made an en­cour­aging dis­cov­ery. One of the rules that defined our dis­char­ging pro­ced­ure was too ri­gid. Re­lax­ing the rule made the pro­ced­ure con­sid­er­ably more ef­fi­cient.

With the new dis­char­ging pro­ced­ure it looked as though we could build an un­avoid­able set whose re­du­cible con­fig­ur­a­tions would be smal­ler than those pro­duced by earli­er pro­ced­ures. The com­puter time re­quired for the proof would prob­ably be less than pre­vi­ous es­tim­ates in­dic­ated. It was still evid­ent, however, that a con­sid­er­able com­pu­ta­tion­al ef­fort would be re­quired to pro­duce even the best un­avoid­able set of re­du­cible con­fig­ur­a­tions. Ed­ward F. Moore of the Uni­versity of Wis­con­sin had de­veloped a power­ful meth­od for con­struct­ing maps that con­tained no small re­du­cible con­fig­ur­a­tions. For ex­ample, he had cre­ated a map in which the ring size of the smal­lest re­du­cible con­fig­ur­a­tion is 12 [see Fig­ure 12]. There­fore any un­avoid­able set of re­du­cible con­fig­ur­a­tions must have at least one con­fig­ur­a­tion of ring size 12. Moore’s work provides a lower bound on ring size, but we now feel sure that a ring size of 13 is ne­ces­sary, and it is quite likely that a ring size of 14 is also ne­ces­sary. (Our proof demon­strates that no lar­ger con­fig­ur­a­tions are needed.)

Figure 12. Map of 846 countries created by Edward F. Moore of the University of Wisconsin is colored with four colors in order to illustrate the four-color theorem. Although some maps (including this one) are fairly difficult to color with four colors, no one has ever created a map that requires five or more colors. Until last year, however, all known efforts to prove that four colors are enough to color any map drawn on a sphere or plane had failed. The difficulty of coloring a map depends on the way in which its countries border on one another. The “configurations,” or arrangements of neighboring countries, within Moore’s map helped the authors estimate the computational difficulties of implementing their ultimately successful approach to proving the four-color theorem. Only part of Moore’s map is shown in the illustration. The complete map is a cylindrical projection with octagons (that is, countries with eight neighbors) at the north and south poles. Moore’s map is composed of 54 octagons, 228 heptagons, 96 hexagons and 408 pentagons. It was colored by Tom Burket.

In Janu­ary, 1976, we began the con­struc­tion of an un­avoid­able set of re­du­cible con­fig­ur­a­tions by means of our new dis­char­ging pro­ced­ure. The fi­nal ver­sion of the pro­ced­ure had one fur­ther ad­vant­age for en­sur­ing the re­du­cib­il­ity of the fi­nal con­fig­ur­a­tions. The pro­ced­ure was es­sen­tially self-modi­fy­ing; the pro­gram was de­signed to identi­fy crit­ic­al, or prob­lem, areas — con­fig­ur­a­tions that looked as though they would res­ist re­duc­tion ef­forts — and to modi­fy it­self to move pos­it­ive charge to a dif­fer­ent place. Since we were do­ing the dis­char­ging pro­ced­ure without the com­puter, we knew that the pro­ced­ure could be mod­i­fied as we en­countered crit­ic­al areas.

We began by mak­ing an ap­prox­im­a­tion, a pre­lim­in­ary run of our dis­char­ging pro­ced­ure. We con­sidered each pos­sible case in which a ver­tex was forced to be pos­it­ive, and in each case the neigh­bor­hood was ex­amined to find an obstacle-free con­fig­ur­a­tion. If none was found, the neigh­bor­hood was called crit­ic­al, which meant that the dis­char­ging would have to be mod­i­fied to avoid this prob­lem. Even when an obstacle-free con­fig­ur­a­tion was found, however, we could not guar­an­tee a re­du­cible con­fig­ur­a­tion. The new re­duc­tion pro­grams were used to try to find some obstacle-free con­fig­ur­a­tion in the neigh­bor­hood that was also re­du­cible. If none was found, the neigh­bor­hood was also called crit­ic­al.

This meth­od of de­vel­op­ing an un­avoid­able set of re­du­cible con­fig­ur­a­tions (as we per­fec­ted a dis­char­ging pro­ced­ure) was only pos­sible by an­oth­er dia­logue with the com­puter. To de­term­ine which neigh­bor­hoods were crit­ic­al it was ne­ces­sary to check for re­du­cib­il­ity quickly, in terms of com­puter time and in terms of real time. For­tu­nately it was sel­dom ne­ces­sary to wait more than a few days for res­ults, even though of­ten a con­sid­er­able amount of com­puter time was needed. Since this in­tens­ive man-ma­chine in­ter­ac­tion was in­dis­pens­able to our work, we should ex­plain the cir­cum­stances that made it pos­sible.

Al­though our ar­range­ment for com­puter us­age seemed quite nat­ur­al to us at the time, we have since dis­covered that we were in­deed for­tu­nate to be work­ing at the Uni­versity of Illinois, where a com­bin­a­tion of a large com­put­ing es­tab­lish­ment and an en­lightened policy to­ward the re­search use of com­puters gave us an op­por­tun­ity that seems to be un­avail­able at al­most any oth­er uni­versity or re­search es­tab­lish­ment. Al­though we could not guar­an­tee that our work would lead to a proof of the four-col­or the­or­em, we were giv­en well over 1,000 hours of com­puter time in what we feel was an ad­mir­able dis­play of faith in the value of pure math­em­at­ic­al re­search. We were in­formed by the com­puter cen­ter that be­cause the uni­versity’s com­puters were not fully util­ized at all times by class work and oth­er kinds of re­search we could be in­cluded in a small group of com­puter users who were al­lowed to share the sur­plus com­puter time. We now know that this policy was es­sen­tial to our suc­cess.

In June, 1976, we com­pleted our con­struc­tion of an un­avoid­able set of re­du­cible con­fig­ur­a­tions. The four-col­or the­or­em was proved. We had used 1,200 hours of time on three dif­fer­ent com­puters. The fi­nal dis­char­ging pro­ced­ure differed from our first ap­prox­im­a­tion by some 500 modi­fic­a­tions res­ult­ing from the dis­cov­ery of crit­ic­al neigh­bor­hoods. The de­vel­op­ment of the pro­ced­ure re­quired the hand ana­lys­is of some 10,000 neigh­bor­hoods of ver­tices of pos­it­ive charge and the ma­chine ana­lys­is of more than 2,000 con­fig­ur­a­tions. A con­sid­er­able part of this ma­ter­i­al, in­clud­ing the re­duc­tion of 1,482 con­fig­ur­a­tions, was used in the fi­nal proof. Al­though the dis­char­ging pro­ced­ure (without the re­duc­tions) can be checked by hand in a couple of months, it would be vir­tu­ally im­possible to veri­fy the re­duc­tion com­pu­ta­tions in this way. In fact, when we sub­mit­ted our pa­per on the proof to Illinois Journ­al of Math­em­at­ics, its ref­er­ees checked the dis­char­ging pro­ced­ure from our com­plete notes but checked the re­du­cib­il­ity com­pu­ta­tions by run­ning an in­de­pend­ent com­puter pro­gram.

Many math­em­aticians, par­tic­u­larly those edu­cated be­fore the de­vel­op­ment of high-speed com­puters, res­ist treat­ing the com­puter as a stand­ard math­em­at­ic­al tool. They feel that an ar­gu­ment is weak when all or part of it can­not be re­viewed by hand com­pu­ta­tion. From this point of view the veri­fic­a­tion of res­ults such as ours by in­de­pend­ent com­puter pro­grams is not as con­vin­cing as the check­ing of proofs by hand. Tra­di­tion­al proofs of math­em­at­ic­al the­or­ems are reas­on­ably short and highly the­or­et­ic­al — the more power­ful the the­ory, the more el­eg­ant the proof — and re­view­ing them by hand is usu­ally the best meth­od. But even when hand-check­ing is pos­sible, if proofs are long and highly com­pu­ta­tion­al, it is hard to be­lieve that hand-check­ing will ex­haust all the pos­sib­il­it­ies of er­ror. Fur­ther­more, when com­pu­ta­tions are suf­fi­ciently routine, as they are in our proof, it is prob­ably more ef­fi­cient to check ma­chine pro­grams than to check hand com­pu­ta­tions.

Figure 13. Postage meter stamp is used by department of mathematics at University of lIIinois at Urbana-Champaign to honor the solution of four-color-map problem by two of its members.

If many math­em­aticians are dis­turbed by long proofs, it may be be­cause un­til quite re­cently they only em­ployed the kinds of meth­ods that pro­duce short proofs. We still do not know wheth­er or not a short proof of the four-col­or the­or­em can be found. Sev­er­al new proofs of mod­er­ate length have been an­nounced, but none of them has sur­vived ex­pert scru­tiny. Al­though it is con­ceiv­able that one of these proofs is val­id, it is also con­ceiv­able that the only cor­rect proofs will be based on un­avoid­able sets of re­du­cible con­fig­ur­a­tions and that they will there­fore re­quire com­pu­ta­tions that can­not be done by hand. We be­lieve that there are the­or­ems of great math­em­at­ic­al in­terest that can only be proved by com­puter meth­ods. Even if the four-col­or the­or­em is not such a prob­lem, it provides a good ex­ample of what might be done to prove one. There is no reas­on to be­lieve that there is not a large num­ber of prob­lems call­ing for this dif­fer­ent kind of ana­lys­is.

Our proof of the four-col­or the­or­em sug­gests that there are lim­its to what can be achieved in math­em­at­ics by the­or­et­ic­al meth­ods alone. It also im­plies that in the past the need for com­pu­ta­tion­al meth­ods in math­em­at­ic­al proofs has been un­der­es­tim­ated. It is of great prac­tic­al value to math­em­aticians to de­term­ine the powers and lim­it­a­tions of their meth­ods. We hope that our work will fa­cil­it­ate pro­gress in this dir­ec­tion and that this ex­pan­sion of ac­cept­able proof tech­niques jus­ti­fies the im­mense ef­fort de­voted over the past cen­tury to prov­ing the four-col­or the­or­em.