Теорема о четырёх красках¶

Теорема о четырёх красках — это утверждение в топологии и теории графов, согласно которому любую карту, расположенную на плоскости или сфере, можно раскрасить не более чем четырьмя цветами так, чтобы любые две соседние области (имеющие общий участок границы ненулевой длины) были разного цвета. Теорема является одной из наиболее известных и долго остававшихся недоказанными математических проблем, впервые сформулированной в середине XIX века и окончательно доказанной в 1976 году с использованием компьютерных вычислений.

¶История

¶Формулировка и первые попытки

Вопрос о минимальном количестве цветов, необходимых для раскраски карты, впервые был поставлен в 1852 году студентом Университетского колледжа Лондона Фрэнсисом Гатри. Он заметил, что для раскраски графства Англии достаточно четырёх цветов, и предположил, что это верно для любой карты. Гатри поделился гипотезой со своим братом Фредериком, который, в свою очередь, передал её математику Огастесу де Моргану. Де Морган опубликовал задачу в научных кругах, но не смог её решить.

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

¶Ложные доказательства

В 1879 году английский математик Альфред Кемпе опубликовал доказательство теоремы, которое было признано верным на протяжении 11 лет. Кемпе ввёл понятие «неизбежного набора конфигураций» и разработал метод «цепей Кемпе», позволяющий перекрашивать карты. Однако в 1890 году Перси Хивуд обнаружил ошибку в доказательстве Кемпе: метод цепей не всегда применим к конфигурациям с пятью соседними областями. Хивуд показал, что доказательство Кемпе доказывает лишь то, что для раскраски любой карты достаточно пяти цветов (теорема о пяти красках). Тем не менее, идеи Кемпе легли в основу будущего успешного доказательства.

¶Компьютерное доказательство

В XX веке проблема оставалась нерешённой. В 1976 году математики Кеннет Аппель и Вольфганг Хакен из Иллинойсского университета в Урбана-Шампейн представили доказательство, основанное на компьютерном переборе. Они свели задачу к проверке 1936 (позднее сокращённых до 1476) неизбежных конфигураций, каждая из которых была «раскрашиваемой» — то есть не могла быть частью минимального контрпримера. Доказательство заняло более 1200 часов машинного времени на суперкомпьютере IBM 360. Публикация результатов вызвала дискуссию в математическом сообществе: многие учёные скептически отнеслись к доказательству, полагающемуся на компьютерные вычисления, которые невозможно проверить вручную. Тем не менее, в 1997 году Нил Робертсон, Дэниел Сандерс, Пол Сеймур и Робин Томас представили упрощённое доказательство, также с использованием компьютера, но с меньшим числом конфигураций (633). В 2005 году Георгий Гонтье и Бенджамин Вернер опубликовали формальное доказательство на языке Coq, что подтвердило корректность теоремы с точки зрения формальной логики.

¶Формулировка и основные понятия

¶Формальное определение

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

¶Условия применимости

Теорема применима только к картам, где:

• каждая область является связной (не состоит из нескольких несвязных частей);
• границы между областями имеют ненулевую длину (точка касания не считается соседством);
• карта расположена на плоскости или сфере. Для карт на торе (поверхности с «дыркой») минимальное количество цветов может быть больше — например, для тора требуется до семи цветов.

¶Доказательство

¶Основные этапы

Доказательство Аппеля и Хакена опиралось на два ключевых понятия:

1. Неизбежный набор конфигураций — множество подграфов, таких что любой планарный граф содержит хотя бы один из них.
2. Раскрашиваемость конфигурации — свойство, при котором любой граф, содержащий данную конфигурацию, может быть перекрашен так, чтобы избежать использования пятого цвета.

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

¶Критика и принятие

Первоначально доказательство было встречено скептически из-за невозможности его полной верификации человеком. Однако последующие упрощения и формальные проверки устранили сомнения. В 2020 году группа математиков под руководством Алекса Уилки подтвердила, что доказательство является корректным, хотя и остаётся «неэлегантным» с точки зрения классической математики.

¶Применение

¶Теория графов

Теорема о четырёх красках является фундаментальным результатом в теории графов. Она используется для доказательства других теорем о раскраске графов, а также в задачах, связанных с распределением ресурсов, составлением расписаний и частотным планированием в телекоммуникациях.

¶Картография

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

¶Компьютерные науки

Доказательство теоремы стало одним из первых примеров использования компьютера для решения математической проблемы, что породило дискуссию о природе математического доказательства. Оно также стимулировало развитие формальной верификации и автоматизированного доказательства теорем.

¶Интересные факты

• Теорема о четырёх красках неверна для карт на торе (поверхности с одной дыркой) — для них требуется до семи цветов. Для более сложных поверхностей (с несколькими дырками) минимальное количество цветов определяется формулой Хивуда.
• В 2019 году группа исследователей из Университета Ватерлоо предложила новое, более простое доказательство, основанное на теории графов и не требующее компьютерного перебора, но оно пока не получило широкого признания.
• Теорема часто путают с задачей о четырёх цветах, которая является её частным случаем. В бытовом смысле «четыре краски» означают, что для раскраски любой карты мира достаточно четырёх цветов, но на практике карты часто содержат эксклавы (например, Аляска для США), что требует дополнительных цветов, если эксклавы считаются частью основной области.

¶Критика

Основная критика теоремы связана с её доказательством, которое невозможно проверить без помощи компьютера. Некоторые математики, такие как Поль Эрдёш, выражали сомнение в том, что компьютерное доказательство является «настоящим» доказательством, поскольку оно не даёт интуитивного понимания причины истинности утверждения. Однако большинство современных математиков признают доказательство корректным, хотя и отмечают его громоздкость.