Проблема четырех красок

Как и множество математических парадоксов, знаменитая Проблема четырех красок возникла в области, на первый взгляд, далекой от математики. В 1852 году англичанин Фрэнсис Гатри (по утверждениям одних, составляя карту британских графств, по утверждениям других, очевидно, на досуге, раскрашивая ее) неожиданно для себя выяснил, что, имея в наличии всего лишь четыре краски, он может совершенно свободно раскрасить карту таким образом, что две соседние области не будут окрашены в один и тот же цвет. С увлечением предаваясь этому занятию, через некоторое время Гатри задал себе вопрос: а что, если не только карты британских графств, но и любая другая карта с любым количеством областей может быть раскрашена с использованием минимального числа красок — четырех, и при этом две граничащие области не будут иметь общую окраску. Возможно ли это? Так родилась Проблема четырех красок.

Поломав некоторое время голову над придуманной самим же проблемой, Гатри «перепоручает» ее знаменитому Уильяму Гамильтону — ирландскому математику и физику, который, пытаясь «изобрести» карту, для раскрашивания которой потребовалось бы более четырех цветов, потерпел неудачу, но тем не менее оставил вопрос открытым, не поставив под окончательное сомнение существование такой карты.

С этого момента проблема четырех красок — одновременно необыкновенно простая и удивительно сложная — начала свое триумфальное шествие по миру. В 1879 году Альфред Кемпе предложил доказательство, которое некоторое время считалось верным, но в 1890 году Перси Хивуд обнаружил в нём ошибку. Хивуд при этом доказал более слабую теорему: для любой карты достаточно пяти цветов.

В течение XX века математики постепенно сокращали число конфигураций, которые необходимо было проверить, и доказывали теорему для всё более широких классов карт.

В 1976 году Кеннет Аппель и Вольфганг Хакен дали первое полное доказательство теоремы четырёх красок с существенным использованием компьютерной проверки конечного набора конфигураций. Это доказательство вызвало дискуссию из-за необычной для того времени роли компьютера, но сама теорема сегодня считается доказанной. В 1990-х годах было получено более простое компьютерно-проверяемое доказательство.