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

Появление теоремы о четырех цветах и ее суть

Первоначально вопросом четырех цветов заинтересовался студент Фредерик Гатри, который изучал карту графств Англии. Гатри заметил, что для того, чтобы два соседних графства были разных цветов, необходимо всего четыре цвета. Это наблюдение заставило его задаться вопросом, возможно ли применить этот принцип к любой карте, будь то весь мир, страна или группа островов.

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

Теория графов в контексте теоремы о четырех цветах 

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

  • сколько ребер нужно, чтобы соединить все вершины;

  • существует ли способ путешествовать по ребрам и посещать каждую вершину только один раз;

  • какой кратчайший путь от одной вершины к другой.

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

Задача раскраски карты может быть преобразована в задачу раскраски графа
Задача раскраски карты может быть преобразована в задачу раскраски графа


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

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

Пример планарного графа
Пример планарного графа

Доказательства теоремы о четырех цветах

Первая попытка доказать теорему о четырех цветах была предпринята юристом Альфредом Кемпе в 1879 году. Ниже мы подготовили его набросок аргументации, которая изложена в современных терминах с использованием графов вместо карт.

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

Предположим, что можно раскрасить все простые планарные графы с n вершинами не более чем четырьмя цветами — это тривиально для n меньше 5. Теперь рассмотрим граф с n+1 вершинами. Как показать, что и она будет раскрашиваться не более чем в четыре цвета?

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

Если удалить эту вершину и все ее ребра, то останется граф с n вершинами, который может быть раскрашен четырьмя цветами
Если удалить эту вершину и все ее ребра, то останется граф с n вершинами, который может быть раскрашен четырьмя цветами

Теперь посмотрим на вершины, соседние с удаленной. Если они имеют три или менее цветов, то мы можем раскрасить удаленную вершину одним из оставшихся цветов.

Мы только что показали, что граф с n+1 вершинами может быть раскрашен четырьмя цветами. Если соседние вершины включают все четыре цвета, то Кемпе придумал  метод перекраски некоторых вершин, чтобы освободить цвет для удаленной вершины, и снова доказал, что для графа с n+1 вершиной требуется всего четыре цвета.

В 1890 году математик Перси Хоуд выявил случай, в котором метод Кемпе не сработал. Несмотря на неудачу, работа Хоуда доказала, что любая карта может быть раскрашена пятью или меньшим количеством цветов. Он также расширил задачу на карты, нарисованные на более сложных поверхностях, и доказал, что для карты на пончике с g отверстиями может потребоваться 12(7+√1+48g) цветов.

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

Но даже когда была доказана теорема Хивуда для общих поверхностей, проблема четырех красок осталась нерешенной.

Компьютерные вычисления и консерватизм математического сообщества

В 1976 году Вольфганг Хакен и Кеннет Аппель при содействии Джона Коха сообщили о доказательстве теоремы. Их подход заключался в разбиении шести частных случаев Кемпе на 1936 подслучаев, каждый из которых проверял компьютер.

На конференции в 1976 году, через 124 года после постановки проблемы четырех цветов, реакция в зале была неоднозначной. «Я ожидал, что аудитория разразится бурными овациями, но вместо этого они ответили вежливыми аплодисментами», — написал Дон Альберс, который присутствовал на выступлении. Возможно, это произошло потому, что вместо того, чтобы приводить аргументы на бумаге, команда в большей степени опиралась на вычисления компьютера.

Математическое сообщество с неохотой приняло результаты. Ученые не были готовы отдать логические рассуждения машине и считали, что доказательство должно быть понятным и проверяемым исключительно человеком. Консерватизм и нежелание принимать достижения, которые позволяют экономить время, не были чем-то новым.

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

Доказательство четырехцветной задачи было только началом компьютерной революции в математике. В 1998 году Томас Хейлз с помощью компьютера доказал  гипотезу Иоганна Кеплера. В ней говорилось, что наиболее эффективный способ укладки сфер — тот, который обычно используют для укладки апельсинов в продуктовом магазине.

В июле 2010 года исследователям с помощью компьютера удалось найти «алгоритм Бога». Оказалось, что максимальное количество поворотов, которое необходимо для решения кубика Рубика — это 20 поворотов граней или 26, если половину поворотов считать за два.

Вопросы цветности непланарных графов

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

Полный граф с n вершинами имеет хроматическое число n
Полный граф с n вершинами имеет хроматическое число n


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

Применение теории графов в других областях

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

Судоку — это замаскированная проблема раскраски графов. Каждую клетку можно рассмотреть как вершину, а девять цифр — как цвета.

Из каждой вершины выходит 20 ребер — по одному к каждой клетке в строке, в столбце и в подквадрате 3 на 3. Этот граф из 81 вершины и 810 ребер начинается с частичной раскраски (заданные подсказки). Задача игры — раскрасить остальные вершины
Из каждой вершины выходит 20 ребер — по одному к каждой клетке в строке, в столбце и в подквадрате 3 на 3. Этот граф из 81 вершины и 810 ребер начинается с частичной раскраски (заданные подсказки). Задача игры — раскрасить остальные вершины

Доказать оригинальную теорему пока никому не удалось

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

Комментарии (6)


  1. Actaeon
    25.07.2023 15:18

    Подумалось: а ведь для доказательства нельзя использовать rust - ну просто потому, что существует только одна реализация языка, и всегда остается вероятность ошибки в компиляторе. Потом, открываю страницу Coq - и о , ужас,там - тоже одна реализация !
    Если здесь есть математики, подскажите вы с 76 года привыкли ходить по льду ??


    1. youngmysteriouslight
      25.07.2023 15:18

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

      Это как с подписью транзакций в блокчейне: задача решается долго, а решение проверяется быстро.

      При наличии этого принципа не важно, одна там реализация Coq или их несколько, ведь всегда можно проверить, что порождаемый ею результат корректен.

      Для Rust такого нет, AFAIK.


    1. domix32
      25.07.2023 15:18
      +1

      Ну, мягко говоря язык и доказательство маленько не соотносятся. И всё зависит от того что именно вы хотите доказать. Для программистов нужны одни доказательства, для математиков - несколько иные. Количество SAT-решателей для разных языков огромно на самом деле и есть подозрение, что сама логика решалок не настолько сложна как доказательства поверх них. Так что вы можете использовать и раст и сишечку и name-your-thing. Буквально сегодня в ленту попало например вот это.


  1. azTotMD
    25.07.2023 15:18

    Про это есть рассказ. Мартин Гарднер - "Остров пяти красок"


    1. Wesha
      25.07.2023 15:18

      Тот рассказ про другую задачу (A) — "сколько максимально может быть цветов, чтобы территория некоего цвета касалась территорий всех остальных цветов, при условии, что все области неразрывны (состоят из единственного куска)". А здесь обсуждается задача (B) "можно ли раскрасить любую карту, используя только четыре цвета, таким образом, чтобы ни одна из двух соседних областей не имела одинакового цвета (но не-соседние области могут быть одного цвета, то есть условия неразрывности тут нет).


      1. domix32
        25.07.2023 15:18

        Фактически можно переформулировать это как задачу четырех красок для полносвязного (читать - не планарного) графа.