Одной из самых известных и в то же время самых противоречивых теорем в истории математики является «Теорема о четырёх красках» (Four Color Theorem). Это утверждение, достаточно простое для понимания даже школьником — «какую бы плоскую карту мы ни взяли, для раскраски её смежных областей в разные цвета достаточно четырёх красок», — потребовало для своего доказательства более века времени и смены парадигмы в виде «компьютерного доказательства», потрясшего сами основы математики как науки.

В этой статье мы подробно, с математической, исторической и философской точек зрения, раскроем всю картину теоремы о четырёх красках: от наивного вопроса в 1852 году, через попытки и неудачи гениев, и вплоть до достижений современной математики, привлекшей на свою сторону новый интеллект — компьютер. В частности, мы углубимся в такие сложные математические темы, как геометрическая структура ложного доказательства Кемпе и контрпримера Хивуда, полное доказательство теоремы о пяти красках, математика метода разрядки (discharging method), алгоритм Аппеля и Хакена, подробности формального доказательства с помощью Coq, а также связь с NP-полнотой.

Глава 1: 1852 год, наивный вопрос Фрэнсиса Гутри и возвышение до теории графов

Постановка задачи о раскраске карт

История начинается в 1852 году и восходит к молодому человеку по имени Фрэнсис Гутри, только что окончившему Университетский колледж Лондона. Раскрашивая карту графств Англии, он заметил один странный факт: «Какой бы сложной ни была карта, не достаточно ли четырех цветов, чтобы раскрасить соседние графства в разные цвета?»

Фрэнсис поделился этим вопросом со своим младшим братом Фредериком Гутри, который в то время изучал математику в Университетском колледже. Фредерик, в свою очередь, представил эту задачу своему научному руководителю Огастесу де Моргану, одному из ведущих математиков того времени. Де Морган сразу же увлекся этой задачей и поделился ей в письме со своим другом Уильямом Роуэном Гамильтоном. Именно этот момент стал рождением сияющей в истории математики «Проблемы четырёх красок».

Теорема Эйлера о многогранниках и двойственность планарных графов

Для того чтобы строго математически подойти к задаче о раскраске карт, необходимо её сформулировать в терминах теории графов. Если каждую область (страну или графство) на карте представить как «вершину» (Vertex), а соседние области соединить «ребром» (Edge), мы получим «планарный граф» (Planar Graph), рёбра которого не пересекаются на плоскости. Это преобразование известно как операция взятия «двойственного графа» (Dual Graph). Границы оригинальной карты соответствуют рёбрам графа, а грани — вершинам.

Проблема четырёх красок сводится к задаче раскраски вершин графа (Vertex Coloring Problem): «Можно ли раскрасить вершины любого планарного графа в 4 цвета так, чтобы смежные вершины имели разные цвета?».

Здесь исключительно важную роль играет теорема о многогранниках, открытая Леонардом Эйлером. В связном планарном графе, если количество вершин равно $V$, количество рёбер — $E$, а количество граней — $F$, то выполняется следующее инвариантное соотношение:

Комбинируя эту теорему с базовыми свойствами планарных графов, можно вывести строгие ограничения на структуру планарных графов. Предположим, что это простой граф без кратных рёбер и петель, и рассмотрим «максимальный планарный граф» (Maximal Planar Graph), в котором все грани являются треугольниками. Любой планарный граф можно превратить в максимальный планарным граф добавлением рёбер, и при этом хроматическое число не увеличится, поэтому достаточно доказать теорему о четырёх красках для максимальных планарных графов.

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

Подставив это в формулу Эйлера и исключив $F$: подставляя $F = \frac{2}{3}E$ в $V - E + F = 2$, получаем:

В общем простом планарном графе грани могут быть ограничены тремя или более рёбрами, поэтому $3F \leq 2E$, что приводит к следующему неравенству:

Это неравенство показывает, что существует строгий верхний предел плотности рёбер планарного графа. Отталкиваясь от этого, давайте подумаем о степени (Degree, $\deg(v)$) каждой вершины. Сумма степеней всех вершин графа ровно в два раза больше количества рёбер (Лемма о рукопожатиях).

Используя предыдущее неравенство $2E \leq 6V - 12$, получаем:

Разделив обе стороны на количество вершин $V$, получим среднюю степень вершин:

Тот факт, что средняя степень строго меньше 6, является математически полным доказательством того, что «по крайней мере одна вершина должна иметь степень 5 или меньше». Иными словами, в любом простом планарном графе существует хотя бы одна вершина со степенью 1, 2, 3, 4 или 5. Этот факт является наиболее фундаментальной отправной точкой для концепции «неизбежной конфигурации», обсуждаемой позже, и абсолютным краеугольным камнем доказательства теоремы о четырёх красках.

Глава 2: «Доказательство» Альфреда Кемпе и его крах 11 лет спустя

Концепция цепей Кемпе и блестящее «доказательство»

В 1879 году Альфред Брэй Кемпе (Alfred Kempe), британский адвокат и математик, наконец опубликовал «доказательство» проблемы четырёх красок в журналах «Nature» и «American Journal of Mathematics». Его доказательство было чрезвычайно оригинальным и принималось мировым математическим сообществом как правильное в течение последующих 11 лет.

Сутью доказательства Кемпе была революционная идея, ныне известная как «цепь Кемпе» (Kempe Chain). Он использовал метод математической индукции. Он предположил, что теорема о четырёх красках выполняется для всех планарных графов с количеством вершин $k$, и попытался показать, что она выполняется и для графов с количеством вершин $k+1$.

Из вышеупомянутой теоремы Эйлера следует, что в планарном графе $G$ с количеством вершин $k+1$ обязательно существует вершина $v$ со степенью не больше 5. Рассмотрим граф $G'$, полученный из графа $G$ удалением вершины $v$ и прилегающих к ней рёбер. Поскольку в $G'$ количество вершин равно $k$, по предположению индукции его можно раскрасить в 4 цвета (пусть это будут красный, синий, зеленый и желтый). Затем мы пытаемся вернуть $v$ и раскрасить её.

1. Если степень $v$ равна 3 или меньше: Вершина $v$ смежна максимум с тремя вершинами. Следовательно, по крайней мере один из 4 цветов не используется смежными вершинами. Достаточно раскрасить $v$ в этот неиспользованный цвет, и доказательство завершено.
2. Если степень $v$ равна 4: Предположим, что 4 вершины, смежные с $v$ (обозначим их по часовой стрелке $v_1, v_2, v_3, v_4$), раскрашены в разные цвета (красный, синий, зеленый, желтый). Теперь рассмотрим подграф, состоящий только из вершин, окрашенных в «красный» и «зеленый» цвета, и рёбер, соединяющих их в исходном графе. Если $v_1$ (красная) и $v_3$ (зеленая) не соединены в этом красно-зеленом подграфе (т.е. нет пути от $v_1$ до $v_3$, проходящего только через красные и зеленые вершины), то можно инвертировать цвета (красный на зеленый, зеленый на красный) в компоненте связности, содержащей $v_1$. Это называется «инверсией цепи Кемпе». После инверсии $v_1$ становится зеленой, и цвета вокруг $v$ сокращаются до трех: синий, зеленый, зеленый, желтый. Теперь можно раскрасить $v$ в красный цвет. Если же $v_1$ и $v_3$ соединены, то в силу топологических свойств планарного графа (теорема Жордана о кривой) красно-зеленый путь, соединяющий $v_1$ и $v_3$, разделяет $v_2$ (синяя) и $v_4$ (желтая). Следовательно, $v_2$ и $v_4$ абсолютно не могут быть соединены сине-желтой цепью Кемпе, и можно инвертировать сине-желтую компоненту, содержащую $v_2$. В любом случае количество цветов вокруг $v$ сокращается до 3, и $v$ можно раскрасить.
3. Если степень $v$ равна 5: Предположим, что 5 вершин $v_1, v_2, v_3, v_4, v_5$ вокруг $v$ раскрашены соответственно в красный, синий, зеленый, желтый, красный цвета (поскольку их 5, один цвет повторяется). Кемпе утверждал, что расширив логику для случая степени 4 и искусно комбинируя инверсии двух различных цепей Кемпе (например, красно-зеленой и красно-желтой), можно обязательно сократить количество цветов вокруг $v$ до 3 или меньше. Его метод дважды применял логику: если одно соединено, то другое разделено.

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

Граф-контрпример Хивуда: фатальный недостаток «пересечения двойных цепей Кемпе»

Однако в 1890 году 29-летний математик по имени Перси Джон Хивуд (Percy John Heawood) внимательно прочитал статью Кемпе и обнаружил фатальный скачок в логике рассуждений относительно вершины степени 5.

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

Хивуд построил конкретный граф-контрпример (максимальный планарный граф из 25 вершин, известный сегодня как «граф Хивуда» или его производные). В этом графе при применении алгоритма Кемпе для сокращения цветов вокруг вершины $v$ степени 5 было показано, что в момент инверсии сине-зеленой цепи ранее не соединенная сине-желтая цепь соединяется, и при последующей инверсии сине-желтой цепи ранее инвертированная зеленая вершина возвращается к своему исходному цвету, в результате чего возникает цикл, в котором количество цветов не уменьшается.

«Одновременная перестановка двойных цепей Кемпе» оказалась ошибкой, возникшей из-за недооценки сложного переплетения планарных графов, при котором локальное топологическое разделение не может поддерживаться глобально. Это открытие привело к полному краху доказательства теоремы о четырёх красках Кемпе.

Полное математическое доказательство теоремы о пяти красках

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

Теорема: Любой планарный граф $G$ можно раскрасить в 5 цветов. Доказательство: Используем метод математической индукции по количеству вершин $n$. Случай $n \leq 5$ тривиален. Предположим, что все планарные графы с $n=k$ могут быть раскрашены в 5 цветов, и рассмотрим планарный граф $G$ с $n=k+1$. Согласно факту, вытекающему из формулы Эйлера, в $G$ обязательно существует вершина $v$ степени не более 5. Граф $G' = G - \{v\}$, полученный удалением $v$ из $G$, имеет $k$ вершин, поэтому по предположению индукции его можно раскрасить в 5 цветов (цвет 1, цвет 2, цвет 3, цвет 4, цвет 5). Рассмотрим возвращение вершины $v$ с сохранением раскраски $G'$.

• Случай 1: $\deg(v) < 5$. Поскольку $v$ смежна не более чем с 4 вершинами, по крайней мере один из 5 цветов не используется смежными вершинами. Достаточно раскрасить $v$ в этот цвет.
• Случай 2: $\deg(v) = 5$. Предположим, что 5 смежных с $v$ вершин $v_1, v_2, v_3, v_4, v_5$ (расположенных по часовой стрелке) раскрашены в разные цвета (соответственно цвет 1, 2, 3, 4, 5). (Если один и тот же цвет используется более одного раза, останется хотя бы один неиспользованный цвет, которым можно раскрасить $v$). Теперь в графе $G'$ рассмотрим индуцированный подграф, состоящий только из вершин, окрашенных в цвета 1 и 3, и обозначим через $C_{13}$ компоненту связности, содержащую $v_1$ (это и есть цепь Кемпе).
  • Подслучай 2a: $v_3 \notin C_{13}$. То есть не существует пути от $v_1$ до $v_3$, проходящего только через вершины цветов 1 и 3. В этом случае, если мы инвертируем цвета всех вершин в $C_{13}$ (цвет 1 $\leftrightarrow$ цвет 3), правильность раскраски сохранится. После инверсии $v_1$ получит цвет 3, а поскольку $v_3$ также имеет цвет 3, цвет 1 больше не будет присутствовать вокруг $v$. Таким образом, $v$ можно раскрасить в цвет 1.
  • Подслучай 2b: $v_3 \in C_{13}$. То есть существует путь $P_{13}$, соединяющий $v_1$ и $v_3$ и состоящий из вершин цветов 1 и 3. Этот путь $P_{13}$ вместе с вершиной $v$ и ребрами $(v, v_1), (v, v_3)$ образует замкнутую кривую (цикл) на плоскости. По свойству планарных графов (теорема Жордана о кривой) этот цикл делит плоскость на внутреннюю и внешнюю части. Вершины $v_2$ и $v_4$ находятся по разные стороны этого цикла (одна внутри, другая снаружи). Теперь рассмотрим цепь Кемпе $C_{24}$, состоящую из вершин, окрашенных в цвета 2 и 4. Если предположить, что $v_2$ и $v_4$ соединены этой цепью, должен существовать путь $P_{24}$, соединяющий $v_2$ и $v_4$. Однако путь $P_{24}$ должен проходить по планарному графу без пересечений, но не может пересечь цикл, образованный $P_{13}$ (что противоречит определению планарного графа). Следовательно, пути между $v_2$ и $v_4$ из цветов 2 и 4 абсолютно не существует. Другими словами, цепь Кемпе $C_{24}$ цветов 2-4, содержащая $v_2$, не включает $v_4$. Поэтому, если инвертировать цвета в $C_{24}$ (цвет 2 $\leftrightarrow$ цвет 4), $v_2$ получит цвет 4, и цвет 2 исчезнет из окружения $v$. В итоге $v$ можно будет раскрасить в цвет 2.

Таким образом, в любом случае вершину $v$ можно раскрасить, и методом математической индукции теорема о пяти красках полностью доказана. $\blacksquare$

Это доказательство прекрасно использует топологию планарных графов (теорему Жордана о кривой) и демонстрирует, насколько мощным является понятие «цепей Кемпе» Кемпе при применении к одиночным непересекающимся цепям. Однако путь к «четырем краскам» отсюда пройдет через новые парадигмы — «сводимость» и «неизбежные множества» — и погрузится в невероятное море вычислений.

Глава 3: Математика метода разрядки (Discharging Method) и вывод неизбежных конфигураций

После Хивуда математики начали исследовать методом от противного структуру, которую должен (или не должен) иметь гипотетический «минимальный контрпример (Minimum Counterexample), не раскрашиваемый в четыре цвета». Здесь становятся важными две мощные концепции: «сводимая конфигурация (Reducible Configuration)» и «неизбежное множество (Unavoidable Set)».

Сводимость (Reducibility)

Сводимая конфигурация — это локальная подконфигурация (паттерн) вершин, которая «абсолютно не может существовать в графе, если он целиком не раскрашивается в четыре цвета (является минимальным контрпримером)». Например, «вершина степени 3 или меньше» и «вершина степени 4» являются сводимыми конфигурациями. Это потому, что, как описано выше, используя редукцию с помощью цепей Кемпе, если бы они существовали, проблему можно было бы свести (редуцировать) к меньшему графу, что противоречит предположению о «минимальном контрпримере». В 1913 году Джордж Дэвид Биркгоф (George David Birkhoff) доказал, что конкретная конфигурация из 6 вершин, называемая «алмазом Биркгофа», также является сводимой. Открытие сводимых конфигураций продолжалось, но без гарантии их «обязательного присутствия» в графе доказательство не могло быть завершено.

Математическая структура метода разрядки (Discharging Method)

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

Чрезвычайно мощным оружием для построения и доказательства этого неизбежного множества стал «Метод разрядки (Discharging Method)», усовершенствованный Генрихом Хеешем (Heinrich Heesch). Метод разрядки — это словно магический прием для доказательства структурных теорем в теории графов, использующий по аналогии концепцию электрического заряда из электромагнетизма.

Математический процесс метода разрядки выглядит следующим образом:

1. $$ch(v) = 6 - \deg(v)$$

   Из уравнения, вытекающего из формулы Эйлера, $\sum_{v} (6 - \deg(v)) = 12$, общая сумма начальных зарядов всего графа строго равна 12 (положительное значение). При этом вершины степени 5 имеют заряд $+1$, вершины степени 6 имеют $0$, а вершины степени 7 и выше имеют отрицательный заряд. (Поскольку мы можем предположить, что в минимальном контрпримере нет вершин степени 4 и ниже, минимальная степень считается равной 5).

2. Определение правил перемещения заряда (Discharging Rules): Затем определяются правила, по которым заряд перемещается между смежными вершинами. Основная идея заключается в том, чтобы «передать (разрядить) заряд от вершин с положительным зарядом (т.е. вершин степени 5) к вершинам с отрицательным зарядом (вершинам высоких степеней, от 7 и выше)». Например, устанавливаются десятки или сотни детальных правил вроде: «Если вершина $v$ степени 5 смежна с вершиной $u$ степени 7, переместить заряд $\frac{1}{5}$ от $v$ к $u$».

3. $$ \sum_{v \in V} ch'(v) = 12 > 0 $$

   (где $ch'(v)$ — заряд вершины $v$ после перемещения) Тот факт, что общая сумма положительна, означает, что «даже после перемещения зарядов должна существовать по крайней мере одна вершина с положительным зарядом».

   Здесь итоговый заряд каждой вершины $ch'(v)$ анализируется на основе её локальной структуры (паттернов степеней самой вершины и её соседей). Если удастся доказать, что «любая вершина, не имеющая определенной конфигурации, при заданных правилах разрядки обязательно будет иметь итоговый заряд ноль или меньше», то для того, чтобы итоговый заряд был положительным, эта «определенная конфигурация» должна обязательно существовать где-то в графе. Список всех таких паттернов локальных конфигураций, дающих положительный итоговый заряд, и образует «неизбежное множество».

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

Глава 4: 1976 год, алгоритм компьютерной верификации Аппеля и Хакена

Определение D-редукции и C-редукции

В 1970-х годах Кеннет Аппель (Kenneth Appel) и Вольфганг Хакен (Wolfgang Haken) из Иллинойсского университета начали исторический проект по объединению метода разрядки Хееша и вычислительной мощи компьютеров.

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

• D-сводимость (D-reducibility / Direct reducibility): Если для всех возможных паттернов 4-раскраски кольцевой границы (Ring), окружающей конфигурацию, их можно расширить на внутреннюю часть конфигурации, либо их можно преобразовать путем инверсии цепей Кемпе на границе в паттерн, который можно расширить внутрь. Если это подтверждается, можно сразу сказать, что эта конфигурация не содержится в минимальном контрпримере.
• C-сводимость (C-reducibility / Contracting reducibility): Метод, показывающий, что если существуют паттерны, не проходящие проверку на D-сводимость, мы можем рассмотреть меньший граф, «стянув» (объединив несколько вершин в одну) часть конфигурации, и если этот стянутый граф раскрашивается в 4 цвета, то и исходный граф также раскрашивается в 4 цвета.

Алгоритм проверки возможности раскраски кольцевой границы

Компьютеру (IBM 360) было поручено выполнение алгоритма проверки на D-сводимость и C-сводимость для огромного числа кандидатов в конфигурации.

Предположим, что некая конфигурация $C$ имеет граничное кольцо $R$ (длиной $k$). Количество комбинаций раскраски вершин кольца в 4 цвета составляет максимум $4^k$, но даже с учетом симметрии это число огромно. Например, при длине кольца $k=14$ необходимо проверить правильность около 200 000 граничных раскрасок. Алгоритм работает по следующим шагам:

1. Сгенерировать множество всех допустимых паттернов 4-раскраски граничного кольца $R$.
2. Перебрать все способы фактической раскраски внутренности конфигурации $C$ в 4 цвета и записать, с какими граничными паттернами они согласуются (можно ли расширить внутрь).
3. Для граничных паттернов, которые нельзя расширить внутрь, симулировать инверсию цепей Кемпе. Если в результате инверсии можно перейти к паттерну, который уже признан «расширяемым внутрь», то исходный паттерн также считается «решенным».
4. Этот поиск переходов инверсии повторяется, и если все граничные паттерны могут быть решены, конфигурация $C$ объявляется «D-сводимой».

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

1200 часов вычислений и «Q.E.D.»

В 1976 году они, наконец, обнаружили неизбежное множество, состоящее из 1936 конфигураций, выведенных с помощью тщательно разработанных правил разрядки. После более чем 1200 часов работы мейнфрейма Иллинойсского университета компьютер подтвердил, что все эти 1936 конфигураций являются D-сводимыми или C-сводимыми.

Они коротко написали в аннотации своей статьи: “Every planar map is four colorable.” (Любая планарная карта может быть раскрашена в четыре цвета.)

На почтовом штемпеле математического факультета Иллинойсского университета была выбита гордая надпись «FOUR COLORS SUFFICE (4 цветов достаточно)». Это было монументальным событием в истории математики: впервые компьютер взял на себя центральные дедуктивные шаги в доказательстве теоремы.

Глава 5: Шок в математическом сообществе и философия «доказательства»

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

Является ли математикой доказательство, которое не может прочесть человек?

В математической традиции, восходящей к Древней Греции, «доказательство» — это то, в чем человек-математик может шаг за шагом проследить логику, глубоко осознать её правильность и быть убежденным. Считалось, что в процессе доказательства кроется глубокое понимание того, «почему теорема верна», и красота структуры.

Однако доказательство теоремы о четырёх красках было иным. В статье был лишь список из 1936 конфигураций и описание компьютерного алгоритма. Реальная трассировка (запись выполнения) проверки на сводимость была настолько огромной, что её даже было трудно распечатать на бумаге. Каким бы гениальным ни был математик, даже за всю свою жизнь он не смог бы отследить эти вычисления вручную и убедиться в отсутствии логических изъянов.

Возникла беспрецедентная ситуация: «Чтобы поверить в правильность доказательства, вы должны поверить, что аппаратное обеспечение компьютера не дало сбой, и что в программе на языке ассемблера, написанной Аппелем и Хакеном, нет багов».

Философ науки Томас Тимочко (Thomas Tymoczko) выступил с критикой, что это доказательство деградировало от чисто математического априорного поиска истины до чего-то эмпирического и экспериментального, подобного физике. Само определение действия «доказательство» оказалось в гносеологическом кризисе.

Контраргументы и упрощение группой RSST

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

Чтобы развеять эти сомнения, многие математики пытались упростить и перепроверить доказательство. В 1997 году Нил Робертсон (Neil Robertson), Дэниел Сандерс (Daniel P. Sanders), Пол Сеймур (Paul Seymour) и Робин Томас (Robin Thomas) (группа, известная как RSST) опубликовали новое доказательство, в котором метод разрядки был сделан более систематическим и удобным для проверки человеком, а размер неизбежного множества был сокращен с 1936 до 633 конфигураций. Это был изящный алгоритм, вычисления которого занимали всего несколько часов.

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

Глава 6: Полное формальное доказательство Жоржа Гонтье с помощью Coq

Как можно математически и полностью развеять страх, что «в программе могут быть баги»? Окончательным ответом стала полная формализация (Formalization) с использованием «Систем интерактивного доказательства теорем (Proof Assistant)».

В 2005 году Жорж Гонтье (Georges Gonthier) из Французского национального института исследований в области информатики и автоматики (INRIA) и Microsoft Research вместе с Бенджамином Вернером (Benjamin Werner) успешно осуществили полную формализацию доказательства теоремы о четырёх красках с нуля, используя систему доказательства теорем «Coq».

Нестандартные конечные отображения (Hypermap) и формализация комбинаторной топологии

Coq — это система, которая описывает и механически проверяет доказательства, отправляясь от математических аксиом и следуя чрезвычайно строгой системе логических правил (Calculus of Inductive Constructions: Исчисление индуктивных конструкций).

Величайшей заслугой Гонтье было то, что он перевел интуитивный и геометрический объект — планарный граф — в полностью алгебраическую и комбинаторную структуру, с которой может работать компьютер. Он определил структуру данных, называемую «гиперкартой (Hypermap)», для представления отношений между вершинами, ребрами и гранями графа. Это метод представления графа как множества «дротиков (полурёбер)» и группы перестановок на них. Таким образом, такие топологические теоремы, как формула Эйлера и теорема Жордана о кривой, были полностью формализованы как комбинаторная логика теории групп и конечных множеств.

Доказательство правильности самой программы доказательства

Более того, Гонтье отбросил «программы верификации, написанные на языке C», созданные Аппелем-Хакеном и RSST, и реализовал сам алгоритм проверки сводимости на внутреннем языке Coq (Gallina). А затем математически доказал в самом Coq правильность алгоритма: «если этот алгоритм проверки выдает “True”, то эта конфигурация действительно является сводимой».

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

Это новая вершина «доказательства» в математике. Это эволюция от «доказательств, которые люди читают и понимают (Informal Proof)» к «формальным доказательствам, логическая полнота которых гарантируется машиной (Formal Proof)». Теорема о четырёх красках стала первой в истории нетривиальной великой теоремой, достигшей этого предельного уровня строгости.

Глава 7: Проблема раскраски планарных графов в 4 цвета и парадокс NP-полноты

Наконец, давайте посмотрим на теорему о четырёх красках с точки зрения теории сложности вычислений (Computational Complexity Theory). Здесь присутствует весьма любопытное парадоксальное явление.

Задача раскраски общих графов (задача определения, можно ли раскрасить заданный граф в $k$ цветов) является одной из самых известных «NP-полных (NP-complete)» проблем в информатике. В частности, доказано, что «задача раскраски планарного графа в 3 цвета (Planar 3-Colorability)» является NP-полной. Другими словами, считается, что алгоритма, определяющего за полиномиальное время, может ли планарный граф быть раскрашен в 3 цвета, не существует, если только $\text{P} = \text{NP}$.

Что же тогда с «задачей раскраски планарного графа в 4 цвета (Planar 4-Colorability)»? Можно интуитивно предположить, что если 3 цвета — это NP-полная задача, то 4 цвета тоже должны быть такой же сложной (NP-полной) задачей.

Однако поразительно, но вычислительная сложность задачи о раскраске планарного графа в 4 цвета (как задачи разрешения) равна $O(1)$, то есть это «константное время (тривиальная задача)». Это потому, что теорема о четырёх красках гарантирует: «все планарные графы можно раскрасить в 4 цвета». Поэтому алгоритму даже не нужно смотреть на входной граф; он может просто вывести «Да», и это всегда будет на 100% правильным ответом. Это прекрасный пример того, как мощная гарантия существования из теоремы снижает сложность задачи разрешения до абсолютного минимума.

Однако это касается только задачи разрешения (Decision Problem) — «можно ли раскрасить». Построение алгоритма раскраски (Search Problem), который «показывает, как именно раскрасить в 4 цвета» — это уже другая история. Если реализовать процедуру доказательства Аппеля-Хакена или RSST в виде алгоритма, мы получим алгоритм, который может фактически найти раскраску в 4 цвета для любого заданного планарного графа с $N$ вершинами. Было показано, что алгоритм, основанный на доказательстве RSST, выводит 4-раскраску за полиномиальное время с наихудшей сложностью $O(N^2)$.

Другими словами, в то время как попытка раскрасить планарный граф в 3 цвета может занять время, равное возрасту Вселенной (NP-полнота), в тот момент, когда мы добавляем 4-й цвет, благодаря математической структуре, лежащей в основе теоремы о четырёх красках, возникает быстрый алгоритм (за $O(N^2)$). Это чрезвычайно загадочный и увлекательный факт, рожденный на пересечении математики и информатики.

Заключение: наследие теоремы о четырёх красках

Наивная задача о раскраске карт, предложенная молодым англичанином в 1852 году, начиналась как простая головоломка. Однако за прошедшее столетие с лишним она открыла огромную новую математическую область — теорию графов, способствовала развитию теории алгоритмов и в конечном итоге поставила перед человечеством фундаментальные философские вопросы: «Могут ли компьютеры доказывать математические теоремы?» и «Что такое математическая истина?».

История теоремы о четырёх красках — это история бурного столкновения пределов человеческой интуиции и возможностей новой логической машины — компьютера. Сегодня и другие грандиозные сложные задачи, такие как гипотеза Кеплера (проект Flyspeck Томаса Хейлза в 2014 году) или теорема Фейта-Томпсона, были полностью доказаны путем формальной верификации с использованием систем интерактивного доказательства теорем.

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