Editing Four color theorem (section)

===Proof by computer===
During the 1960s and 1970s, German mathematician [[Heinrich Heesch]] developed methods of using computers to search for a proof. Notably he was the first to use [[discharging method (discrete mathematics)|discharging]] for proving the theorem, which turned out to be important in the unavoidability portion of the subsequent Appel–Haken proof. He also expanded on the concept of reducibility and, along with Ken Durre, developed a computer test for it. Unfortunately, at this critical juncture, he was unable to procure the necessary supercomputer time to continue his work.{{sfnp|Wilson|2014|pp=139–142}}

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

If the four-color conjecture were false, there would be at least one map with the smallest possible number of regions that requires five colors. The proof showed that such a minimal counterexample cannot exist, through the use of two technical concepts:<ref>{{harvtxt|Wilson|2014|pp=105–107}}; {{harvtxt|Appel|Haken|1989}}; {{harvtxt|Thomas|1998|pp=852–853}}</ref>

# An ''unavoidable set'' is a set of configurations such that every map that satisfies some necessary conditions for being a minimal non-4-colorable [[maximal planar graph|triangulation]] (such as having minimum degree 5) must have at least one configuration from this set.
# A ''reducible configuration'' is an arrangement of countries that cannot occur in a minimal counterexample. If a map contains a reducible configuration, the map can be reduced to a smaller map. This smaller map has the condition that if it can be colored with four colors, this also applies to the original map. This implies that if the original map cannot be colored with four colors the smaller map cannot either and so the original map is not minimal.

Using mathematical rules and procedures based on properties of reducible configurations, Appel and Haken found an unavoidable set of reducible configurations, thus proving that a minimal counterexample to the four-color conjecture could not exist. Their proof reduced the infinitude of possible maps to 1,834 reducible configurations (later reduced to 1,482) which had to be checked one by one by computer and took over a thousand hours. This reducibility part of the work was independently double checked with different programs and computers. However, the unavoidability part of the proof was verified in over 400 pages of [[microfiche]], which had to be checked by hand with the assistance of Haken's daughter [[Dorothea Blostein]].{{sfnp|Appel|Haken|1989}}

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

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