Archives & Special Collections

                                               John Koch, the Four-Color Programmer

Wilkes University Archives has a guest blog post today written by TQ Smith, a sophomore Computational Mathematics major. During Summer 2019, Dr. John Allen Koch donated his materials to the Wilkes University Archives. As part of his internship, TQ processed and created the finding aid for the collection. In addition to this blog post, he also created an in-person exhibit on the first floor of Farley Library in Spring 2020. Here are his reflections:

The Four-Color Conjecture states that every planar graph is four colorable. The problem is simple enough for a grade-schooler to understand. Imagine a map of multiple countries. The conjecture states that the whole map can be colored using four colors such that no adjacent countries have the same color. The only exceptions to this rule are countries that meet at a single point. For example, if five countries intersected at a single point, five colors would be required to color the graph. Therefore, graphs that are similar to a pizza pie or the spokes of a wheel are excluded from the problem.

            The conjecture seems deceptively simple, with an obvious, if not trivial solution. Francis Guthrie originally stated the conjecture in 1852. However, it remained unproven until 1976. Many great mathematical minds attacked the problem, but none prevailed to prove it. The conjecture highlights a fundamental idea of mathematical proof. In order to verify the conjecture, mathematicians would have to prove that every graph could only use four colors. To disprove the conjecture, mathematicians would have to create one graph that used five colors. The difficulty of the problem motivated many to attempt a solution. The more minds that failed, the more infamous the problem became in mathematical history. One could argue that the Four-Color Conjecture accelerated the development in the mathematical field of graph theory.

            I would like to take a moment to talk about my connection with the Theorem. I remember sitting in my high-school classroom, learning about the conjecture, and hearing about the role of the computer in its solution. As an aspiring mathematician and computer scientist, I was intrigued. I wondered about the great programmers that wrote the code. At that time, I knew the code had to be extensive, highly optimized, and eloquently written. The next fall, I was browsing Dr. John Koch’s website, a full professor from the Wilkes University Computer Science department, after my first class. I could not believe what I was reading. The great programmer was my professor! In my excitement, I went to his office hours and discussed the problem with Dr. Koch, and he explained his work to me.

            So, how did the conjecture become a theorem? The answer lies in the hard work of three men at the University of Illinois: Kenneth Appel, Wolfgang Haken, and John Koch. The mathematical machinery employed by these brilliant minds is beyond the scope of this blog. I am hopeful to understand the mathematics they employed at some point in my future career. The basic method of proof used was contradiction. Proof by contradiction assumes that negation of a statement and derives a fallacy. Since an impossible statement is reached, the negated statement must also be false. Thus, the original statement must be true. The two other concepts that one must understand is the unavoidable set and reducible configurations. The unavoidable set is the set of graphs such that one of the graphs must be contained in any planar graph. A reducible configuration is a graph such that any graph containing the reducible configuration as a subgraph can always be four colored. Appel, Haken, and Koch assumed the existence of a graph that was not four colorable. The trio then showed that an unavoidable set of only reducible configurations existed. This contradicted their supposition and proved that any graph is four colorable.

The mathematicians Haken and Appel were using complex computer programs to color graphs and test if a graph is part of the unavoidable set. The supercomputers at the time, now slower than your smartphone, were too slow in executing Haken and Appel’s FORTRAN programs. The pair needed a talented programmer who was able to write the algorithms in assembly language to increase execution speed. They went to the computer science department and found the then graduate-student, John Koch, to write their code. Koch used his work towards his PhD.

            In total, Koch wrote 12,000 lines of code. For those that do not know, programming in the mid-1970s was much different than programming today. Koch did not have a laptop with all of his code on it, nor did he have a personal computer to run the code. Instead, Koch had to write his programs using punched cards. Each line of code corresponds to one punched card. There were miles of code in his collection. Once the program was compiled, the program was stored on magnetic tape.

            When Koch wanted to run the code, he would travel to the university in the evenings. At night, fewer people were running programs, allowing Koch’s programs to utilize all of the computer’s resources. He would let the programs run all night. Since computers were not as reliable in the 1970s, Koch was taking a risk each time he ran a program. The computer could randomly crash and stop executing his program.

When great discoveries such as these are uncovered, many are curious of the ramifications. The proof of the Four-Color Conjecture is a prime example of a discipline-changing discovery. The proof closed a century old problem. Since the conjecture was proven using a computer, many believed that it was a brute-force, ineloquent solution. Some did not recognize its validity. It was the first time someone used a computer to prove a mathematical theorem. In the modern day, no one bats an eye about mathematicians using computers to model drug interactions, weather patterns, protein folding, genetic analysis, or other applications. The proof of the Four-Color Conjecture not only changed the world of computing; the proof of the Four-Color Conjecture changed the world’s view on computing. The whole mathematical community can thank Haken, Appel, and Koch for this development.

Since September 1976, Koch has been a professor at Wilkes. Koch and Dr. Joe Parker are responsible for the development of the Computer Science degree at Wilkes. He has taught numerous classes on a multitude of computational subjects. Also, Koch is credited with popularizing the use of the internet throughout Wilkes. During his time as a professor, Koch dedicated his time to his country. Koch worked for the Institute for Defense Analyses at Princeton, New Jersey, and he retired, in 1998, as a Lieutenant Colonel in the Army National Guard. In his free time, Koch likes to ride his bike and spend time with his family. He is a husband and father of two sons, and he is a grandfather of five grandchildren. I will be forever thankful to Dr. Koch for this opportunity to process and preserve a part of mathematical history and the birth of computational mathematics.