Editor’s note: This article was initially published in The Daily Gazette, Swarthmore’s online, daily newspaper founded in Fall 1996. As of Fall 2018, the DG has merged with The Phoenix. See the about page to read more about the DG.
Thomas Hales of the University of Pittsburgh spoke yesterday in a lecture entitled “Formal Proofs, the four-color theorem, and the Kepler conjecture for sphere packing.”
The four-color theorem states that the greatest number of colors necessary for coloring a map is 4, with no two adjacent regions sharing the same color. While the first proof of this was written in the 1880s, gaps were found shortly after. The problem continued unproven until late in the 20th century, when it became the first major theorem to be proved using a computer.
Hales began the talk with a short explanation of the four-color theorem and then proceeded to explain similar but less complex problems, beginning with the Jordan Curve theorem. This theorem proves that a simple closed curve will divide a plane into exactly two regions–an inside and an outside. While this seems obvious, it is actually extremely hard to prove.
But then Hales added a “bridge” to the picture, connecting the inside to the outside–making only one region total and “disproving” the theorem. He also demonstrated that if you add a similar bridge in a map, the four-color theorem will not hold either.
From the Jordan Curve theorem, Hales went on to describe two more theorems: the “factory” theorem and Euler’s relation. In the “factory” theorem, there are 3 houses and 3 factories, and the goal is to connect all the houses to all the factories without any lines crossing. However, this is not possible as two lines will always cross–unless a “bridge” is added.
Euler’s relation shows that relationship between vertices (V), edges (E), and faces (F) in any closed curve is V – E + F = 2. The can be used to demonstrate the Jordan Curve theorem, as the number of vertices and edges cancel out, leaving the number of faces equal to 2. But again, using a bridge will cancel out Euler’s relation.
Hales used all these examples to show that the four-color theorem requires planarity in order to work, meaning that the map would have to lie in a two dimensional plane, and that any sort of proof would invoke this.
He then went on to discuss formal theorem proving, a new way of developing proofs that he is heavily involved in. He explained that a large problem in writing proofs is the huge number in steps that have to be present in order to prove something all the way down to the fundamentals.
Formal theorem proofs are verified by computers that have both the axioms and inferential steps as well as the proof itself programmed in. The computer is then able to check all the intermediate steps and show that the proof is correct. As more proofs are checked this way, the database grows and further proofs are easily to check.
Hales has used this process to check his own proof of the Jordan Curve theorem and plans to do the same thing for his recent proof of Kepler’s conjecture. He digressed briefly to discuss this problem, which states that the most efficient way to stack balls in 3-D space is a pyramid.
Finally, Hales returned to the four-color theorem and discussed the most recent proof completed last December by Georges Gonthier. But he then scrapped his entire buildup of the Jordan Curve theorem and Euler’s conjecture, as the new proof involved none of these techniques. Instead it used a different theory of hyperspaces, which ironically makes all the other theorems easier to solve. Hales then spent a few minutes explaining how hyperspaces worked, and then wrapped up his lecture.
Questions continued for ten minutes afterwards, clarifying issues dealing with formal theorem proving and the use of computers.