Теорема о четырёх красках утверждает, что любую карту, нарисованную на плоскости, можно раскрасить не более чем четырьмя цветами так, чтобы никакие две области с общей границей не имели одинаковый цвет. Две области, которые соприкасаются только в одной точке, могут быть одного цвета. Теорема верна для любой карты, какой бы сложной она ни была.
Области 1, 2, 3 и 4 граничат с несколькими другими. Левая область цвета 4 и правая область цвета 4 не имеют общей границы, поэтому им можно дать один цвет. Здесь действительно нужны все 4 цвета.
Фрэнсис Гатри высказал эту гипотезу в 1852 году, раскрашивая карту английских графств. Он заметил, что четырёх цветов всегда будто бы хватает, но доказать это не смог. Проблема сопротивлялась математикам 124 года. Было опубликовано много неверных доказательств. Пяти цветов всегда достаточно, и это можно доказать вручную с помощью формулы Эйлера для планарных графов.
От первого подозрения до доказательства прошло 124 года. Доказательство 1976 года стало первой большой математической теоремой, подтверждённой компьютером.
Доказательство Кеннета Аппеля и Вольфганга Хакена 1976 года стало первым большим математическим доказательством, опирающимся на компьютер. Оно свело все возможные карты к 1936 конфигурациям и поручило компьютеру проверить каждую из них, затратив более 1200 часов процессорного времени. Многих математиков смущало доказательство, которое нельзя проверить вручную от начала до конца. Человеко-читаемое доказательство, если оно существует, до сих пор не найдено.
Пять внешних областей, то есть нечётное число, заставляют кольцо использовать 3 цвета: цикл длины 5 невозможно раскрасить всего в 2 цвета. Центральная область граничит со всеми пятью внешними и соприкасается со всеми тремя цветами кольца. Поэтому ей нужен четвёртый цвет. Это показывает, что четыре цвета иногда действительно необходимы.
Любую карту на плоскости можно раскрасить не более чем четырьмя цветами так, чтобы никакие две области с общей границей не имели одинаковый цвет. Фрэнсис Гатри сформулировал гипотезу в 1852 году. Аппель и Хакен доказали её в 1976 году, проверив 1936 конфигураций на компьютере, и сделали её первой большой теоремой с компьютерной поддержкой. Более короткая проверка Робертсона, Сандерса, Сеймура и Томаса в 1997 году сократила число конфигураций до 633. На торе теорема уже неверна: там иногда требуется семь цветов.