THE FOUR-COLOR THEOREM
Robin Thomas · 2002
Can the countries of a planar map be colored using four colors in such a way that countries sharing a boundary segment (not just a point) receive different colors? This simply stated question, formulated by Francis Guthrie in 1852, turned out to be one of the hardest problems in mathematics. The history of the problem includes many false proofs, a long list of equivalent formulations and a lot of theory it inspired. A complicated and computer-assisted proof was finally found by Appel and Haken in 1976, but it is not completely satisfactory. A simpler but still computer-assisted proof was obtained by Robertson, Sanders, Seymour and the speaker. The quest for a computer-free proof continues. The talk will discuss all of the above aspects at a level suitable for the mathematically-inclined members of the general public. In particular, the speaker will explain how a computer can prove a mathematical theorem.