Представьте себе географическую карту поверхности планеты (шара), на которой есть только суша; каждая точка поверхности принадлежит какой-то стране. Все страны односвязные — представляют собой единый кусок без дырок.
Картографу нужно раскрасить карту так, чтобы никакие две соседние страны не были одного цвета. Соседние страны — это такие, у которых есть общая граница ненулевой длины; если у двух стран только одна общая точка границы, то они могут быть одноцветными.
Как много красок нужно картографу, чтобы раскрасить карту по таким правилам?
Оказывается, четыре, — в этом и состоит утвеждение теоремы о четырех красках.
Но ее долго не могли доказать, и она оставалась известной как задача о четырех красках. Считается, что в середине XIX века ее поставил Фрэнсис Гутри в письме своему брату.
Она хорошо переводится на язык графов. Представьте, что у вас есть раскрашенная карта; сожмите каждую страну до одной цветной точки, и соедините точки отрезками, если у этих стран есть общая граница. Получится граф, у которого ребра не пересекаются (планарный); концы всех ребер разноцветные. Мало того: у этого графа нет петель (страна не граничит сама с собой) и нет двойных ребер (у двух стран только одна граница).
В терминах графов теорема о четырех красках звучит так:
Для любого планарного графа без петель и кратных ребер можно раскрасить его вершины в 4 или менее краски так, что у любого ребра концы разноцветные.
В формулировке важно, что раскрашивать нужно именно сферу. Например, чтобы раскрасить по таким правилам тор, может потребоваться 7 красок, а чтобы раскрасить ленту Мёбиуса — 6 красок.
Источник картинок:https://ru.wikipedia.org/wiki/Теорема_о_четырёх_красках
Доказывали теорему долго. Несколько раз публиковались, а потом опровергались доказательства. Были получены серьезные неочевидные результаты о других поверхностях; и только поверхность шара никак не поддавалась.
И только в 1974 году Аппель и Хакен с применением компьютера показали, что четырех красок достаточно, и это вызвало серьезный раздрай в математическом сообществе. Ведь ни один человек доказательство не мог проверить вручную, своими собственными силами! Мало того, в алгоритме 1974 года обнаружилась ошибка, пришлось в него вносить исправления. Текст доказательства занимал около 500 страниц с картинками; и только к 1981 году Шмидт проверил процентов 40% ключевых 400 страниц, исправив по дороге 15 ошибок. Похоже, что ни один человек так никогда и не проверил даже текстовую часть доказательства до конца.
В конце концов стало ясно, что проще создать новое доказательство, чем довести до безупречного состояния доказательство Аппеля и Хакена. Позднее это сделал Пол Сеймур. У него и компьютер был помощнее, и алгоритм более устойчивый.
Доказательство Аппеля и Хакена было первым компьютерным доказательством в математике. И до сих пор такой подход остается неоднозначным; общепринятым его тоже нельзя назвать. Когда мы знакомимся с чужими доказательствами, то узнаем что-то новое, знакомимся с какими-то новыми приемами. Мы получаем новое понимание и усваиваем (ощущаем своим) новое знание. Компьютерные доказательства ничего такого нам не дают; и потому оставляют ощущение незавершенности и даже «компьютерных махинаций» — по словам Дэниэля Коэна