# 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.

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.

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.

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.

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.

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].

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.

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.

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.

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.

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.

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.)

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.

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.