Насколько мне известно, а известно мне это от профессора Идо Эфрата, не все математики принимают "компьютерные доказательства". При чём, он имел в виду не "автоматические доказательства теорем", а именно перебор вариантов, когда, к примеру, доказательство теоремы разбивают на разные случаи, большинство доказывается в общем виде, а часть доказывается с помощью простого перебора вариантов. Если мне не изменяет память, одна из так называемых теорем "о раскраске" доказана таким образом, а также часть теорем в теории Галуа.
При этом он объяснял причину такого скепсиса. Нет, это не проблема округления. Дело в том, что и процессор и память на физическом уровне могут привести к сбою к вычисление. Грубо говоря, иногда у компьютера 2+2 может быть 5. Бывает это крайне редко, вероятность этого содержит очень много нулей. Однако, когда производят очень много математический вычислений, такой сбой может произойти. В частности, при распределённых вычислениях, это обстоятельство учитывается. Google, обрабатывает столько информации, что у него есть специальные алгоритмы, которые позволяют находить эти ошибки. Обычно, однако, просто повторяют вычисления ещё раз, иногда, на компьютерах другой архитектуры. Если получают разный результат - был сбой, если один и тот же, то вероятность ошибки очень сильно сокращается и её обычно пренебрегают.
Именно поэтому, никогда нельзя быть до конца уверенным, что в компьютерном доказательстве нет ошибки. Единственный способ, по Идо Эфрату, это проверить, это повторить все вычисления, шаг за шагом в ручную.
UPDATE: Реальный пример сбоя работы памяти, любезно предоставленный Ильёй Весенним.
UPDATE: Как мне указали в комментариях, "одна из так называемых теорем "о раскраске"" является проблемой четырёх красок.
UPDATE 17-08-2014:
Компьютер проверил доказательство гипотезы Кеплера
У человека вероятность сделать ошибку еще больше. Так что если в теореме присутствует ручной перебор, то его нужно проверять компьютером.
ReplyDelete>Единственный способ, по Идо Эфрату, это проверить, это повторить все вычисления, шаг за шагом в ручную.
ReplyDeleteНаверняка сам Идо Эфрат в этот момент добавляет, что так мы избавляемся от вероятности компьютерной ошибки, но приобретаем вероятность ошибки человека, который будет проводить вычисления шаг за шагом.
halyavin, Илья Весенний, видимо я не очень удачно выразился. Конечно, если теорему перепроверить один человек, то вы правы, однако, если это по силам одному человеку, то это наверняка сделают и большее количество людей и тогда ситуация не будет ничем отличаться от обычной ситуации с доказательством теорем. Когда один человек считает, что доказал что-то, а потом другой перепроверяя его находит или "дыры" в доказательстве или ошибки. Чем больше человек просмотрят такое доказательство, чем меньше вероятность, что там всё ещё вкралась ошибка.
ReplyDeleteВ обычной ситуации любой желающий может переправить, в случае с компьютером, объёмы вычислений могут быть такие, что ни одному человеку повторить их не под силу.
Какая бредовая аргументация у вашего профессора :) Вероятность ошибки даже у перепроверяющих людей куда больше. Хуже того, наверняка наиболее вероятно не то, что процессор ошибётся, а то, что в программе ошибка (опять же, человеческая).
ReplyDeleteКстати, я не вижу разницы между перебором всех вариантов (естественно, их тогда должно быть конечное множество) и автоматическим доказательством теоремы. И то и другое - строгое математическое доказательство, и в то и в другое может вкрасться ошибка.
Другое дело - вероятностное доказательство вроде метода Монте-Карло, тут уж неудивительно если его не все принимают.
Кстати, о компьютерных сбоях:
ReplyDeletehttp://www.popmech.ru/article/7131-mutatsiya/ - вот пример случайного глюка одного бита. Такое очень даже бывает. Поэтому стоит ждать сбоя и в компьютерных доказательствах.
Илья Весенний, во-первых, спасибо за линк, я его вставил в тело заметки. Во-вторых, посчитайте сколько времени эта память бесперебойно работает, сколько вычислений на ней делалось, чтобы понять, что это вероятность-таки мала. Другое дело, что в ракетостроении её тоже учитывают. Делают это, в частности, за счёт избыточности систем. Почему с Voyager 2 этого не было сделано, вот в чём настоящая загадка. ;-)
ReplyDeleteThe Four color theorem -
ReplyDelete"http://en.wikipedia.org/wiki/Four_color_theorem"
is currently proved by a computer.
Anonymous, спасибо, я добавил ссылку на русскую вики в тело поста.
ReplyDeleteЛюбопытно, что Аппеля и Хакена (авторов компьютерного доказательства теоремы о четырех красках) таки вынудили это самое доказательство опубликовать. В результате появилась книга с названием, если я не путаю, "Every planar graph is four-colorable". В ней 741 страница, и она вся полностью посвящена изложению этого самого доказательства.
ReplyDeleteМне довелось держать эту книгу в руках, но, конечно, внимательно я ее не просматривал. Вообще сомневаюсь, что ее кто-нибудь внимательно прочитал, включая авторов.
Собственно, иногда возникающему вопросу "Как можно доверять доказательству, которое проделано компьюьтером?" можно противопоставлять встречный: "Как можно доверять доказательству, которое написано на бумаге?"