Как бесконечную задачу свели к конечной

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

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

Что именно проверял компьютер

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

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

Почему это изменило саму проверку доказательств

В 1976 году Кеннет Аппель и Вольфганг Хакен сообщили о доказательстве, опиравшемся на компьютерную проверку. Результат вызвал новый вопрос: если ключевую часть рассчитал компьютер, как людям убедиться, что он проверил всё правильно? Полностью перепроверить каждую машинную операцию вручную было бы практически нереально.

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