Обсуждение проблемы четырёх красок

[beroal]

Отделено от процитированной темы:

Klad33 в сообщении #482269 писал(а):

Меня потрясла задача четырех красок. Нужно так разукрасить произвольные страны на карте, чтобы никакие страны с одинаковым цветом не оказались смежными. Вопрос стоял о минимальном количестве красок для раскраски любой, самой фантастичной, карты. Несмотря на простоту задачи, доказать ее теоретически так и не удалось. Удалось только проверить при помощи ЭВМ путем перебора всех вариантов (их больше 1000).

Тут какое-то недоразумение. AFAIK количество карт бесконечно. Так что её всё-таки доказали. Просто на ЭВМ можно проверять и доказательства, причём не только из теории графов.

[Portnov]

Количество карт бесконечно, но все карты можно разделить на конечное (очень большое) количество классов, таких что карты внутри одного класса в определённом смысле эквивалентны (т.е. если мы умеем раскрашивать одну карту из класса, то мы умеем раскрашивать и все остальные карты того же класса). И вот эти классы перебирала уже машина, и для каждого из них строила доказательство возможности раскраски. Это у меня, конечно, очень поверхностное описание доказательства :) Афаик, результирующее доказательство получилось под 500 страниц. Вот, кстати, одна из актуальных проблем современной математики: доказательства, которые кое-как можно построить, но нельзя понять и проверить без помощи машины (просто потому, что они слишком большие).

[Klad33]

Вот что интересно: только описание алгоритма расчета на ЭВМ заняло 741 стр. Не исследован был вопрос о возможных сбоях в самой машине. Нужно было бы в качестве проверки эту же задачу рассмотреть, составив другую программу и рассчитав на принципиально другом компьютере. Этого не было сделано, так как никто не взял на себя смелость разобраться в потугах 1976 года. Так что доказательство данной задачи - это бабушка надвое сказала.

[PAV]

Klad33 в сообщении #482421 писал(а):

Нужно было бы в качестве проверки эту же задачу рассмотреть, составив другую программу и рассчитав на принципиально другом компьютере.

И что бы такая "проверка" доказала?

[beroal]

Portnov в сообщении #482382 писал(а):

Количество карт бесконечно, но все карты можно разделить на конечное (очень большое) количество классов, таких что карты внутри одного класса в определённом смысле эквивалентны (т.е. если мы умеем раскрашивать одну карту из класса, то мы умеем раскрашивать и все остальные карты того же класса).

Говорить, что теорему доказали путём перебора всех вариантов — это большое упрощение. Такое доказательство сможет выполнить и программист.

-- Mon Sep 12, 2011 12:49:26 --

Klad33 в сообщении #482421 писал(а):

никто не взял на себя смелость разобраться в потугах 1976 года

Вы бы хотя бы почитали Википедию. Доказательство упрощалось и переделывалось. Следовательно, кто-то разбирался.

[Klad33]

Разбирались в отдельных деталях, но не глобально. Википедия - это не настолько серьезная вещь, чтобы ей верить полностью. Вы же это сами прекрасно знаете.
Меня вот что сейчас заинтересовало: имеет ли практическое значение проблема 4-х красок? Ну, естественно, кроме составления политической карты мира на планете Земля. Я примеров, увы, не знаю. Может, кто-то более осведомлен?

[alex1910]

beroal в сообщении #482425 писал(а):

Такое доказательство сможет выполнить и программист.

Программист - не сможет. Сложность его наивного алгоритма будет запредельная.

Собственно, средний программист не сможет даже решить систему линейных уравнений с достаточно большой (полагаю, уже матрицы 50*50 хватит, чтобы к ней был неприменим наивный метод Гаусса) матрицей, не прибегая к специальной литературе по методам вычислений.

[beroal]

Klad33 в сообщении #482421 писал(а):

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

Этот вопрос конечно интересный, но только с академической точки зрения. Если говорить о случайных сбоях, то понизить влияние такого сбоя можно, запустив ту же программу на том же компьютере. Если говорить о систематических сбоях, типа Pentium fdiv bug, то здесь поможет proof checker. Prover выдаёт доказательство, которое проверяется proof checker-ом. Существование такой ошибки в процессоре, что prover выдаёт неправильное доказательство, и proof checker оценивает его как правильное, маловероятно.

-- Mon Sep 12, 2011 13:01:45 --

alex1910 в сообщении #482428 писал(а):

beroal в сообщении #482425 писал(а):

Такое доказательство сможет выполнить и программист.

Программист - не сможет (1). Сложность его наивного алгоритма (0) будет запредельная.

Это поразительно, как вы ничтоже сумняшеся выдаёте противоречивое высказывание. Вы говорите, что программист сможет написать алгоритм (0) и в то же время что не сможет (1). Мне с вами не о чём разговаривать.

[Klad33]

Ба! Я погуглил и нашел, что проблема 4 красок в этом форуме уже разбиралась! Но там все сводилось к анализу графов: topic32755.html

[beroal]

Portnov в сообщении #482382 писал(а):

Вот, кстати, одна из актуальных проблем современной математики: доказательства, которые кое-как можно построить, но нельзя понять и проверить без помощи машины (просто потому, что они слишком большие).

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

-- Mon Sep 12, 2011 13:11:39 --

Klad33 в сообщении #482431 писал(а):

Ба! Я погуглил и нашел, что проблема 4 красок в этом форуме уже разбиралась! Но там все сводилось к анализу графов: topic32755.html

Да, лучше бы выделить наш разговор в отдельную тему (это просьба к модераторам). Но в указанной вами теме разбиралось самопальное доказательство, а не официальное. Если бы официальное доказательство можно было бы так сильно упростить, мы бы об этом узнали, я полагаю.

[Klad33]

beroal в сообщении #482432 писал(а):

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

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

PS. Да, мы слишком увлеклись. Я пожалуй остановлюсь.

[beroal]

Как бы это объяснить. Проблема осталась, но новая проблема менее проблематична, чем старая. «Всё познаётся в сравнении».

[Portnov]

beroal
Проблема, наверное, действительно «менее проблематична». Хотя есть и другие точки зрения. Вы, наверное, видели эту (популярную) статью: http://elementy.ru/lib/431269?page_design=print («Теоремы софиста Горгия и современная математика»). Автор, видимо, пессимист. Так или иначе, проблема существует.

[Klad33]

Статья классная! Огромное спасибо. Мысли Горгия корреспондируются с моими предположениями насчет проблем математики. Но есть, думаю, верный путь - предельно упростить математику. Как это уже однажды было, когда от римских чисел перешли к арабским.

[alex1910]

beroal в сообщении #482429 писал(а):

Это поразительно, как вы ничтоже сумняшеся выдаёте противоречивое высказывание. Вы говорите, что программист сможет написать алгоритм (0) и в то же время что не сможет (1). Мне с вами не о чём разговаривать.

Beroal, никому не нужен алгоритм сам по себе - всем нужен результат работы алгоритма. Если этот результат достижим через триллион лет - значит задача не решена.