Hales explains the four-color theorem, formal proofs

October 6, 2005

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.

Sample advertisement

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.

Leave a Reply

Your email address will not be published.

Previous Story

New Wasserstein play features Swarthmore in a supporting role

Next Story

Maragaret Dorsey speaks on music and media

Latest from Sports

Athlete of the Week: Olivia McClammy ’25

Swarthmore softball standout Olivia McClammy ’25 has not only been stealing bases but also the attention of many for record-shattering effort. The senior utility player currently holds a handful of all-time program records, her first of the season on March 1, when

A Personal Reflection on Sports: Similar but Different

As the school year comes to a close, Swarthmore athletes begin to clear out of their team locker rooms and reflect on their respective season. Cleats, jerseys, sneakers, hair bands – these everyday items trickle out of the Field House day by

Athlete of the Week: Aidan Sullivan ’26

Aidan Sullivan ’26 is a junior outfielder from Cos Cob, CT, on the baseball team. The Canterbury High School graduate is a psychology and mathematics double major. Outside of the classroom he is a baseball game changer. Sullivan has broken the program
Previous Story

New Wasserstein play features Swarthmore in a supporting role

Next Story

Maragaret Dorsey speaks on music and media

The Phoenix

Don't Miss