The Four-Colour Theorem

The "Four-Color Theorem" or the "Four-Color Problem" was first formulated in 1852 by the South African mathematician Francis Guthrie (1831-1899) when he attempted to color the counties of England on a map in such a way that no two adjacent regions received the same color. It was obvious that three colors were not sufficient for this task. On the other hand, Guthrie could not construct an example where five colors were needed. But is it always the case that four colors are sufficient, mathematically proving that regardless of the shapes and sizes of the regions?

Although many mathematicians attempted to solve the problem, it took 124 years until 1976 when American mathematicians Kenneth Appel and Wolfgang Haken found a proof with the help of a computer, reducing the number of problematic cases from infinite to ultimately 1,476. Then, in 2004, a formal proof was constructed using a software program called "Coq," rendering the need for verifying remaining individual cases unnecessary.

The Four-Color Theorem was the first major mathematical problem to be solved with the aid of computers. However, the proof was not universally accepted by all mathematicians because it cannot be directly replicated by a human, relying instead on the correctness of the compiler and hardware. The mathematical elegance of the proof was also criticized: a good proof reads like a poem - this one looks like a phone book.