Теорема о четырёх красках
Теоремы в математике бывают самые разные и порой возникают из вполне практических задач.

В 1852 Фрэнсис Гутри составлял карту графств Англии и заметил, что хватает всего четырёх красок. Из этого факта родилась теорема:

Всякую расположенную на плоскости или на сфере карту можно раскрасить не более чем четырьмя разными цветами (красками) так, чтобы любые две области с общим участком границы имели разный цвет.

Уточнения:
- область не может состоять из нескольких отдельных «кусков», каждый из них будет считаться отдельной областью;
- в теореме речь про области, у которых есть общая граница ненулевой длины; если у двух областей только одна общая точка границы, то они могут быть и одноцветными.

Переводя на язык географии: никаких эксклавов и никакой воды (под неё бы потребовался ещё один цвет).

Точно ли хватит четырёх красок?
Доказать теорему долгое время не удавалось. В конце XIX века доказали, что всегда будет достаточно пяти цветов, но для четырёх дело шло туго.

В итоге доказательство нашли лишь в 1976 году, причём с помощью компьютера. Кстати, это была первая большая теорема, доказанная таким образом.

На первом шаге доказательства авторы продемонстрировали набор из 1936 карт, ни одна из которых не могла содержать карту меньшего размера (которая опровергала бы теорему). Авторы использовали специальную компьютерную программу, чтобы доказать это свойство для каждой из 1936 карт.

Далее шёл вывод, что раз для этих карт нет контрпримера, то его не будет и дальше, так как любая бóльшая карта по сути является лишь склейкой из данных 1936 видов.

Доказательство теоремы заняло несколько сотен страниц! Многие математики были недовольны: это вам не тёплое ламповое «человеческое» доказательство, да и вручную его не проверишь. А ещё в нём потом были найдены ошибки. 😇

К 2005 году ошибки устранили, всё перепроверили несколько раз и сконструировали более простое доказательство, основанное на том же принципе. Количество видов карт удалось сократить до 633. Так что сейчас всё в порядке, теоремой можно пользоваться!