Теорема о 4 красках

Сначала нужно разбить на конечное число классов или свести к рекурсивному случаю, там не совсем в лоб же доказывали.

http://en.wikipedia.org/wiki/Graph_coloring

Это намёк.

Есть код на Coq. А вообще уже есть и более простое человеческое доказательство: http://arxiv.org/abs/math.CO/0408247/

Программа очень простая, например для штатов США:

color(red). color(green). color(blue). color(orange).

neighbor(StateAColor, StateBColor) :- color(StateAColor), color(StateBColor), StateAColor \= StateBColor.

Как доказать, что это работает для любого числа штатов?

Зачем программа, зачем теорема?
Все границы на этой планете сводятся к различным версиям четырёх вариантов, приведенных здесь (те что по углам, хотя там таки один лишний). Доказательство «теоремы» заключается в поиске на планете места, где границы пяти сопредельных государств сходятся так, как показано на центральном фрагменте. Достаточно найти или устроить хоть одно такое место - и теорема зафейлена.

у 2 и 5 нет общего участка границы — они могут быть покрашены в один цвет.

границы пяти сопредельных государств сходятся так, как показано на центральном фрагменте. Достаточно найти или устроить хоть одно такое место - и теорема зафейлена.

достаточно трёх цветов.

Едрить бестолоч.

Да, я что-то протупил с картинками.
Согласно формулировке, если уйти от карт областей к графам (где нода = область, линк = общая грань), с каждой нодой в таком графе непосредственно слинкованными могут быть максимум три соседние ноды.
Это можно себе представить полносвязным графом из 4 нод (эквивалент в виде «цветовых карт» - эмблема гуглохрома, лень рисовать). Если где-то рядом появляется пятая нода со своими линками, то она, согласно формулировке, не сможет быть соседом с какой-то одной из уже имеющихся четырёх нод потому, что изначально мы запретили считать соседями все комбинации стыков на карте, сложнее трёх. Т.е. четвёртый и более линк на ноде у нас означает наличие вокруг ноды «несоседей» без общего линка, у которых цвета уже могут повторяться.
Вот я и не пойму, чего тут доказывать, если ответ в самом условии?

с каждой нодой в таком графе непосредственно слинкованными могут быть максимум три соседние ноды.

Нода «Швейцария» слинкована с пятью другими.

гугли «поиск в глубину».

в данном случае алгоритм такой:

цвета RGBY

1. красим область в R, если нельзя, то в G и т.д.

2. если цвета кончились, то п4

3. если покрасили, то идём в соседнюю белую область, и на п1.

3.1 если красить нечего, то win

4. эту область невозможно покрасить. Делаем её белой, и возвращаемся к прошлой области.

5. если возвращаться некуда, то fail

6. красим область в следующий цвет (если она R, красим в G), и на п1

Нода «Швейцария» слинкована с пятью другими.

потому её можно покрасить в R, а пять других в B G B G Y. Достаточно четырёх цветов.

Достаточно найти или устроить хоть одно такое место

в оригинальном условии оговаривается, что таких мест нет.

Да, но у Швейцарии (5 соседей) и Австрии (4+ соседей) общих нод-соседей только три. В итоге всё скатывается снова до фрактала из полносвязных графов максимум из четырёх нод. С большим числом нод любой фрагмент графа перестаёт быть полносвязным. И всё из-за нашего определения линков/границ.

В итоге всё скатывается снова до фрактала из полносвязных графов максимум из четырёх нод.

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

Глянь на свою картинку: если-бы Австрия оторвала бы центр Лихтенштейна(дорожку к Швеции), то стало бы два Лихтенштейна, которые не граничат друг с другом, и которые всё равно можно покрасить в один цвет. Потому для Австрии и Лихтенштейна достаточно двух цветов. И ещё один для их соседа(соседей) общих с Швецией.

В принципе, единственное, что должна будет искать программа, доказывающая эту теорему - это наличие в предварительно построенном графе карты мира кластеров из >4 нод, который окажется полносвязным. Если такой найдётся, значит
а) мы неправильно построили граф и он в этом месте не соответствует карте мира или
б) миф разрушен.

а можно открыть википедию, и прочитать:

Теорема о четырёх красках была доказана в 1976 году Кеннетом Аппелем (англ.) и Вольфгангом Хакеном (англ.) из Иллинойского университета. Это была первая крупная математическая теорема, доказанная с помощью компьютера.

А ещё можно посмотреть кино или послушать песню и забыть об этом.
Но лучше попробовать понять суть, не правда ли?

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

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

Подробности можно найти тут: http://en.wikipedia.org/wiki/Four_color_theorem

Мне в двадцатом веке было намного сложнее с этим разобраться, кстати.

Я помнится разбирался в этой проблеме, там не сложно.

Ну вот, ты же тоже зачем-то разбирался сам, а не тупо прочитал, что «всё уже украдено до нас», и забил.

Ну вот, ты же тоже зачем-то разбирался сам, а не тупо прочитал

я не сам разбирался. А по книжкам. И не «тупо прочитал». Т.ч. решение задачи для меня достаточно очевидно.

Если тебе интересен вопрос, то советую тоже почитать: http://ru.wikipedia.org/wiki/Гарднер,_Мартин

А то на ЛОРе тебе вряд-ли кто-то лучше расскажет.

Спасибо.

Как доказать, что это работает для любого числа штатов?

С чего ты взял, что такой подход решит задачу в общем случае? из вики:

[quoet]Первым шагом доказательства была демонстрация того, что существует определенный набор из 1936 карт, ни одна из которых не может содержать карту меньшего размера, которая опровергала бы теорему.