Спустя 50 лет после первого компьютерного доказательства теоремы четырёх красок группа из шести математиков представила новый вариант доказательства и одновременно существенно усилила сам результат. Авторы показали, что планарный граф можно раскрасить четырьмя цветами почти за линейное время, O(n log n), тогда как лучший предыдущий алгоритм требовал квадратичного времени.
Теорема четырёх красок утверждает, что любую карту на плоскости достаточно раскрасить четырьмя цветами так, чтобы области с общей границей имели разные цвета. На языке теории графов речь идёт о раскраске вершин планарного графа, то есть графа, который можно нарисовать без пересечения рёбер.
Саму теорему не пришлось спасать от ошибки или заново подтверждать после появления сомнений. Первое общепризнанное доказательство Кеннет Аппель и Вольфганг Хакен получили в 1976 году с помощью компьютера, а подробное изложение опубликовали годом позже. В 1990-х Нил Робертсон, Дэниел Сандерс, Пол Сеймур и Робин Томас разработали более компактное компьютерное доказательство и алгоритм раскраски с временной сложностью O(n²).
Главный результат новой работы лежит глубже очередного подтверждения известной теоремы. Прежние доказательства искали в планарном графе хотя бы одну редуцируемую конфигурацию или небольшой препятствующий цикл. Такой участок можно упростить, раскрасить уменьшенный граф, а затем восстановить удалённую часть без нарушения четырёхцветной раскраски.
Новая работа доказывает, что подобных мест в большом планарном графе не одно и не несколько. Их количество растёт линейно вместе с размером графа. Более того, редуцируемые конфигурации удаётся находить почти повсюду, включая большие локально «плоские» участки, где прежние методы практически не давали информации.
Разница принципиальна для алгоритма. Старый подход на каждом шаге уменьшал задачу лишь на некоторое фиксированное число вершин, поэтому множество последовательных сокращений в итоге приводило к квадратичному времени. Новый метод позволяет за один этап убрать постоянную долю графа, после чего задача рекурсивно повторяется для заметно меньшего объекта. Так появляется сложность O(n log n).
Для доказательства авторы используют метод перераспределения зарядов, связанный с комбинаторной кривизной графа. В классических доказательствах локальная положительная кривизна указывала на область, где должна находиться подходящая редуцируемая конфигурация. Новая техника работает и в участках с нулевой кривизной, что авторы называют наиболее существенной новой частью работы.
Цена ускорения оказалась заметной. Доказательство опирается более чем на 8200 D-редуцируемых конфигураций. Для сравнения, доказательство Аппеля и Хакена использовало 1482 конфигурации, а вариант 1996 года сократил набор до 633. Новому методу нужен гораздо больший каталог, поскольку алгоритм ищет не одну подходящую конфигурацию, а линейное число независимых участков по всему графу.
Проверить тысячи вариантов вручную практически невозможно, поэтому значительная часть локального перебора снова выполняется компьютером. Авторы опубликовали исходный код, 8200 файлов с редуцируемыми конфигурациями, 84 правила перераспределения зарядов и программы для проверки вычислительной части доказательства. По их оценке, полный набор проверок на машине с 256 вычислительными ядрами занимает несколько часов.
Авторы отдельно подчёркивают, что работа не является формальным машинным доказательством, полностью записанным в системе автоматической проверки теорем. Математическая аргументация рассчитана на чтение человеком, а конечные и слишком объёмные переборы передаются программам на C++. Исследователи также использовали системы искусственного интеллекта для дополнительной проверки псевдокода и реализации, но прямо отмечают, что такая проверка сама по себе не гарантирует правильность доказательства.
Почти линейная сложность, вероятно, не станет последней точкой. Сейчас основным препятствием остаются цепи Кемпе, последовательности связанных вершин двух цветов, перекрашивание которых требуется при восстановлении удалённых частей графа. Каждая такая операция потенциально затрагивает весь граф. Авторы считают, что предварительная обработка данных позволит выполнить все нужные операции суммарно за O(n) и получить уже полностью линейный алгоритм раскраски.
Новый результат может оказаться шире задачи о картах на плоскости. Найденные плоские области возникают и в больших триангуляциях других фиксированных поверхностей, поэтому разработанные методы потенциально можно перенести на более общие задачи теории графов. Работа уже вошла в программу FOCS 2026.
