Few mathematical theorems are ever covered & publicized to the greater mainstream (aka non-academic) crowd. Sometimes, because, well, math is boring to sane people, but mainly because many of these theorems are brutally convoluted & unnecessarily hard to grasp. The sweet spot between simplicity & significance is rarely found in the general textbook of unsolved math problems; however, the topic of this piece, is one of the rare few exceptions that very much does strike that balance.

The Four Color Theorem, or the Four Color Map Theorem, in its simplest form, states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. As promised, that’s a theorem any elementary-level student can grasp. A second, more math-y form of the theorem states that: given any separation of a plane into contiguous regions producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color. A bit more complicated, but confidently graspable at an undergraduate-level. A third & final way of stating the theorem, that’s vastly more practical but exponentially more complex, requires the language of graph theory. In graph-theoretic language, the four color theorem claims that the vertices of every planar graph can be colored with at most four colors without two adjacent vertices receiving the same color, or, in other words: every planar graph is four­ colorable. Don’t worry if this last description flew over your head, the point is to simply introduce it & preview the connection to graph theory— we’ll take the time to define & digest it later on.

In addition to its inviting simplicity, the Four Color Theorem is famous for its inflection point in the history of math: it was the very first major theorem “proved” through brute-forcing scenarios with a computer. In today’s day-&-age that’s a rather historically-significant breakthrough. As we’ll see shortly, despite a massive entry of theorems since 1852, the Four-Color theorem had outright resisted any attempts at a general conjecture for decades. And even when a likely conjecture reared its head in 1976, the Four-Color Theorem refused to yield to any general map. Which, in turn, forced the latest entrants to turn to this questionable method of provability (computing all scenarios). The implications of accepting this method as a general proof rightly raised questions about what it means to prove a theorem. Indeed, thanks to the Four-Color Theorem, people are still debating the role of computers in mathematical proof & the future of mathematics as a human endeavor.

Before continuing, pause now & take a moment to imagine a complex map that you believe requires more than four colors. Go ahead & quickly sketch it out — then try coloring it in (or filling it in with integers 1–4). Myself included, I’ve yet to come across someone who intuitively believes this theorem at first sight; it just seems false. And yet, throughout its history, not a single counterexample has been discovered. We’ll eventually walk-through the logic of the latest accepted conjecture, however, to satisfy our curiosity for a deeper understanding, we’ll first start at the very origin of the problem.

Origin

The Four Color Theorem burst into the scene as nothing more than a curious observation. First pondered upon by one Francis Guthrie in early 1852, the proposal occurred while trying to color the map of England, when he noticed that only four different colors were needed. Shortly thereafter graduating from the University of London, he went on to study law; by this time, however, his younger brother Frederick Guthrie had become a student of the famed mathematician August De Morgan. Francis shared his original observation as well as his fruitless attempts with Frederick to ask & enroll De Morgan on the quest to bring forth a conjecture.

De Morgan was unable to give an answer, however, as history shows he was instantly hooked. On 23 October 1852, he wrote the following to William Hamilton, a famous Irish mathematician & astronomer:

A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet. He says that if a figure be anyhow divided and the compartments differently coloured so that figures with any portion of common boundary line are differently coloured — four colours may be wanted, but not more — the following is the case in which four colours are wanted. Query cannot a necessity for five or more be invented. …… If you retort with some very simple case which makes me out a stupid animal, I think I must do as the Sphynx did….

De Morgan’s self-deprecating humor towards the end of the letter underlines a stunning bemusement that’s consistent with first impressions of the Four Color Theory. Regardless, with the problem now in the hands of one of the most prominent mathematicians of his generation, it quickly spread like wild-fire; thus, officially sparking the race for a generalized conjecture.

Historical Attempts

After approximately three decades since the observation was first proposed, assistance arrived from one Arthur Cayley. Flustered by the unsolved nature of this seeming-simple problem, Cayley officially enlisted while attending a meeting of the London Mathematical Society; half-way through the meeting, he asked everyone in attendance whether anyone had found a solution. With no one volunteering an attempt let alone a solution, he headed home to face the challenge head-on.

Less than a year later, 1879, Cayley returned with a publication submitted to the Royal Geographical Society (On The Colouring Of Maps). Lacking a proper solution, he nevertheless drastically pushed forth the stagnant search by explaining his shortcomings & attempts at reframing the problem. One of these productive shifts in perspective stemmed from his question: “what if a particular map is already successfully colored with four colors, & we add another area, can we still keep the same coloring?” Essentially an inverse inquiry, it helped start another path towards a general theorem.

Next in the chronicles of the Four-Color Theorem arrived Alfred Bray Kempe. Another London barrister (lawyer) who studied mathematics under Cayley at Cambrige, Kempe attempted his hand at the impossible proof to surprisingly fruitful results. In early July of 1879, Alfred Bray Kempe announced in Naturethat he had a proof of the Four Colour Conjecture.

The core of Kempe’s theorem relied on a proven theorem, a now-common graph theory operation, & a completely original method. The crux of Kempe’s theorem revolved around the proven fact that every planar graph must have a vertex with degree less than six. From this postulate, Kempe’s proof consisted of scrubbing, or patching, sub-graphs of maps by removing vertices with four vertices or less. Why patch out sub-graphs of four vertices or less? Because with four vertices or less, these sub-graphs were undeniably four-colorable. Once all minor (less than four vertices) vertices were patched out, Kempe’s proof consisted of coloring in & uncovering sub-graphs until the original graph remained. The big trick in his proof, his greatest contribution to the effort, was his inventive method of coloring the remaining sub-graphs. Instead of using all four colors, Kempe observed that many, though not all, many adjacent graphs only needed two colors .

The core method of Kemp’s theorem relied on an inventive method of his aptly named Kempe chains. A Kempe chain is a “chain” of vertices that are colored with two alternating colors. Though possible to explain orally, a visual example explains the concept in a much more succinct way. For example, let’s pretend the map of the United States below represents a graph. A Kempe chain is an adjacent, alternating coloring of N units. Below, in our map (graph), we can see adjacent states alternating in colors: New York (Blue), Pennsylvania (Red), Ohio (Blue), Indiana (Red), & Illinois (Blue):

The example above is a clear Blue-Red Kempe chain. It conveys which vertices are colorable with alternating colors; perhaps even more importantly, however, it provides information about which vertices (states) cannot join the current chain, for example, California or Florida (since neither is adjacent to the current chain). These chains served as the backbone of Kempe’s proof of the four-color theorem, by patching out small sub-graphs, then coloring in the remaining maps with Kempe chains. For the longer part of at least a decade, it was believed that Kempe successfully cracked it. Receiving tremendous acclaim, he was elected a Fellow of the Royal Society, served as its treasurer & was shortly knighted.

False Positive

Unfortunately, despite the premature celebrations, as history shows, Kempe’s proof was indeed wrong. The Four Colour Theorem returned to being the Four Colour Conjecture in 1890 with a publication submitted by a lecturer at Durnham, England by the name of Percy John Heawood. He showed that Kempe’s proof was wrong, however, he couldn’t correct the mistake himself:

The aim here is rather destructive than constructive, for it will be shown that there is a defect in the now apparently recognized proof.

The theorem flaw hid in plain sight for over a decade before rearing it’s head, nevertheless, Heawood rekindled the race to prove the four-color theorem.

The next waves of advancement came from across the pond. First, George David Birkhoff, one of America’s first prominent mathematicians, contributed by constraining Kempe’s theorem through finding certain large reducible configurations. From there, Philip Franklin, an MIT mathematician, expanded upon Birkhoff’s work to prove that Four-Color Theorem holds true for all graphs with 25 or fewer vertices. What followed from the 1910s to the 1950s was a flurry of collaborate effort to prove the theorem for graphs with higher & higher vertices; thereby inching slightly closer to a general proof.

By 1968, any counter-example to the Four-Color Theorem must have at least 41vertices. In addition to large reducible configurations, another focus of those on the hunt was a little something called unavoidable sets. The best known method for finding unavoidable sets at the time an approach called discharging, invented by a Heinrich Heesch. Seeing the need for an equilibrium between reducible configurations & unavoidable sets, Heesch was likely the first mathematician who publicly stated a belief that the Four-Color Conjecture could be proved by finding an unavoidable set of reducible configurations. Last, & equally important, Heesch observed that the set necessary could contain up to ten-thousand configurations. Proving ten-thousand scenarios, by hand, unfortunately, required a Herculean physical task. Fortunately, the timing couldn’t have been more perfect as the tide was turning on a previously-niche technology: the burgeoning field of computer science. High-speed computers made such a proof possible.

The Age of Computers

Computers turned out to be exactly the tool our pioneers required to properly test the configurations for reducibility. The complexity of a vertex or map configuration, known as a ring-size, is calculated by the number of vertices “surrounding” or “encapsulating” it. In the early 60s, however, computers were only powerful enough to test figures with ring-size less than 12, — which was insufficient for the proof. Not a programmer himself, Heesh was unaware of this limitation & moved to partner up with a high school teacher by the name of Karl Durre. On November 23, 1965, almost an entire century since it’s inception, the first reducibility test was run on a CDC 1604 — a computer at the Institute of Technology in Hannover, Germany. It was surprisingly successful. After a month of back-testing, the pair tested the program for the first time with a configuration of ring-size nine whose reducibility had been previously unknown. It worked, however, Durre had already noticed that computing resources in Germany would not suffice. So the pair made several trips to the United States to much more powerful computers — yet the problem still remained unsolved. Heesch, frustrated & flustered, finally returned home to Hannover, vowing to finish the proof of the Four-Color Theorem on his own. History responded with a hard nien, however, as due to disagreements with the German research community, he failed to acquire additional funding & resources.

Heesch did, however, manage to metaphorically pass on the torch to a curious student of his. One Wolfgang Haken, an attendee of Heesh’s lectures on the Four Color Theory, gained a lifelong interest in the problem & reached out to Heesch to re-motivate him. It worked. Another two years into their quest, & once again funding became an issue. Heesch, now aging & burnt out, finally threw the towel in. Still enthusiastic but lost without his mentor, Haken declared “Right now I’m quitting. I consider this to be the point beyond which one cannot go.”

It was at this point that, for the final time, that one wearied soldier’s pessimism was outweighed by another soldier’s optimism. Upon hearing about Haken’s resignation, another zealous academic, this time Kenneth Appel, a mathematician & computer programmer professor at the University of Illinois, insisted that he & Haken could finish this journey. Haken, revived by this enthusiasm pressed onward. In the summer of 1976, after several hundred pages of scrutinizing details & over 1200 hours of output on a powerful computer, the four-color conquest finally came to a halt. Appel celebrated the success by etching the statement ‘Modulo careful checking, it appears that four colors suffice’ onto the department’s blackboard. Appel & Haken presented their proof to a group of mathematicians at a meeting in Toronto. Shortly after this presentation, they polished and published the proof, which is lengthy but boils down to checking 1,936 cases for reducibility.

The End?

Fun fact, each of the 1,936 cases required a computer crunch up to 500k logical operations. The controversy of the Four Color Theorem persists: the validity of the proof still remains in question to this day. And for good reason. Mathematicians, & the community as a whole, are now left between a rock & a hard place: come to a consensus in our acceptance of a new, computer-aided type of proof or re-attempt to prove the Four Color Theorem manually.

Regardless of all the skepticism, it was indeed commemorated as a valid proof. The University of Illinois mathematics department adopting the slogan “Four Colors Suffice.” Predictably though, this did not completely end research on the four-color theorem; as a whole, the community is reluctant to cede to the proof as it stands. So, as expected, progress has slowed but never fully stopped. The most recent effort came in 1996, when Neil Robertson, Daniel Sanders, Paul Seymour,& Robin Thomas made a giant leap in reducing the cases of the unavoidable set to only 633 configurations. Though again, this method strongly resembles that of Appel & Haken in which it requires computational checking, it cannot be verified by hand. As David Burton, an associate professor & math historian states:

It cannot be ruled out that a short and convincing proof of the conjecture may yet be found, but it is just as conceivable that the only valid proofs will involve massive computations requiring computer assistance. If this is the case, we must acknowledge that a new and interesting type of theorem has emerged, one having no verification by traditionally accepted methods. Admitting these theorems will mean that the secure notion of a mathematical proof is open to revision.

Perhaps the largest irony in the near-two century-long search for an answer to the Four Color Theory stems from the overall lack of urgency in solving it. Originally stumbled upon by a curious barrister coloring in a map, one would expect that the theorem would be relevant & applicable to cartography: it isn’t so. Cartography has evolved quite smoothly with very little care for the Four Color Theory. Yet, from the many advances in graph theory & the overall push to re-define theorems in modern times, it’s clear that the journey has had measurable outcomes. The ultimate jigsaw puzzle — simple to understand, yet impossible to solve, the Four Color Theorem holds a special place in the history of both math & computer science. Perhaps we may never find an elegant proof to the four-color theorem & it really is an inflection point in the history of theorems. Alas, as always, only time will tell.