![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaТема возникла в комментариях вот здесь. ![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
french_man подробно описал своё (положительное) отношение к использованию компьютерных программ в математических доказательствах здесь (два коммента), за что ему большое спасибо. Я опрометчиво пообещал сделать то же самое: пришлось основательно подумать, чтобы понять, какова же собственно моя позиция по этому поводу. Надумалось довольно много.
Итак, речь идёт о математических теоремах (или, более обще и неопределённо, результатах), в процессе доказательства (получения) которых нетривиальным образом используются компьютерные программы. Уточним: речь идёт о теоремах в "чистой" математике, не требующих априори длинных вычислений (в конце концов, "найдите первый миллион цифр в десятичном разложении пи" тоже ведь математическая задача). Более важно уточнить, что значит "нетривиальным образом": это значит, что заменить запуск программы ручной проверкой не представляется возможным (скажем, такая проверка заняла бы миллион лет).
Канонический пример - знаменитая теорема о раскраске карты в четыре цвета. Дана карта неких областей, скажем, государств, с произвольным размером областей и их количеством. Всегда ли можно раскрасить эту карту, закрашивая каждую область полностью одним цветом, так, чтобы две смежные области всегда были разного цвета, и используя всего 4 цвета?
Все известные доказательства этой теоремы используют компьютерные программы нетривиальным образом. Впервые её доказали Аппель и Хакен в 1976-м году, а недавно было опубликовано новое, более простое доказательство. В обоих случаях доказательство состоит из теоретической части, в которой доказываются некоторые свойства, которыми обязан обладать контрпример, опровергающий теорему (а именно: он должен содержать в себе конфигурацию специального вида, и всего таких возможных конфигураций конечное количество), и компьютерной части, в которой вполне нетривиальный алгоритм перебирает это конечное кол-во конфигураций и проверяет, что ни одна из них не "подходит" для включения в контрпример (я здесь немного упростил, но несущественно).
О доказательствах такого рода можно задать два вопроса:
1. Насколько стоит им доверять? Должны ли они иметь такой же статус, как "обычные" доказательства? Каковы аргументы за или против использования таких доказательств?
Это вопрос философский, относящийся к философии математики.
2. Как к ним в действительности относятся в математическом сообществе? Как к ним относятся математики и какие аргументы выдвигают в поддержку своих мнений?
Это вопрос социологический.
На самом деле, эти два вопроса, конечно же, тесно связаны, и вообще не очень получается думать о них по отдельности. Но я попытаюсь обосновать следующую гипотезу: предлагаемые математиками причины неприятия таких доказательств обычно неубедительны, но, возможно, за чувствами неудобства, неприятия, неуютности, испытываемыми математиками, скрываются другие объективные причины, которыми они сознательно не оперируют и потому не предлагают в качестве объяснений.
french_man предлагает следующий достаточно убедительный список выдвигаемых обычно причин "против" -
а) Формальные: Нет абсолютной точности, т.к. она недостижима в физическом мире (компьютеры ломаются, электроны управляются вероятностями).
б) Концептуальные: Такие доказательства "механичны", не добавляют ничего к нашему пониманию математики.
в) Психологические: неуютно.
- и отвергает их одну за другой. С его возражениями я в принципе согласен, и согласен с тем, что это причины обычно выдвигаемые (вопрос номер 2 выше), но не согласен с тем, что это все возможные причины "быть против" (вопрос номер 1 выше). К особо интересующему меня аргументу можно придти только путём пристального анализа этих, уже выдвинутых, причин.
"Концептуальный" аргумент меня не очень интересует, и принципиальным, на мой взгляд, не является. Не буду на нём останавливаться. "Психологический" аргумент сам по себе аргументом не является - это констатация факта. Математикам "не нравятся" такие доказательства, им неуютно с ними. Но почему не нравятся? - это нужно пытаться объяснить отдельно. Остаётся "формальный" аргумент, кстати, по моему опыту, как раз наиболее часто встречающийся.
А: Я не доверяю компьютеру. Компьютеры ошибаются.
Б: В каком смысле ошибаются?
А: В прямом. Как может моя вера в правильность доказательства зависеть от того, что какая-то там проволока правильно соединилась с другой проволокой и не соскочила?
Б: Но ведь математики тоже ошибаются. Причём постоянно и, пожалуй, куда чаще компьютеров.
А: Ну это потому что они и задачи выполняют куда сложнее компьютерных! И вообще, это другое.
Б: Но почему другое?
А: Не знаю. Но чувствую. Может быть, вот почему: математик сам отвечает за свои ошибки. Это его проблемы, и в идеале, если он постарается, он их обнаружит.
Б: Посадим параллельно компьютер и математика перемножать много 200-значных чисел. Кто больше раз ошибётся? Ответ очевиден. В конце концов, просто с прагматической точки зрения стоит доверять компьютеру. А чувства-шмувства... это просто от привычки. Привыкнем доверять компьютерам - и интуиция изменится.
В этом диалоге А - некий общий образ математика, настроенного "против" компьютерных доказательств, а Б - математика, настроенного "за", и использующего примерно те же аргументы, что высказалfrench_man. Оба математика, однако, упускают одну важную деталь. Какую?
Мы доверяем не компьютеру, а алгоритму.
Эту мысль надо пояснить. Более строго скажем так: нашу веру (или неверие) в то, что компьютер выдаёт правильный результат после решения поставленной перед ним задачи, можно (и нужно, непременно нужно!) разбить на две части:
1. Мы доверяем алгоритму, составленному для решения задачи. Это значит, что мы верим в то, что алгоритм действительно правильно её решает. Алгоритм - математический объект.
2. Мы доверяем инженерам, сконструировавшим компьютер. Это значит, что мы верим в то, что компьютер безошибочно выполняет алгоритм. Компьютер - физическое устройство.
Первая составляющая нашего доверия - исключительно математическая, абстрактная. Вторая составляющая - исключительно физическая, прагматическая.
Давайте убедимся в том, что первая составляющая действительно существует и реальна. Вопрос: почему математик не боится умножать в столбик? Ведь умножение в столбик - это тоже алгоритм, во время выполнения которого думать не надо, а надо глупо следовать правилам. Ответ: потому что математик доверяет алгоритму. Он знает (и может строго доказать), что если взять число X и число Y, и провести с их десятичными представлениями некоторое количество странных сложений, сдвигов и переносов "в уме", то получится десятичное представление числа X*Y. Именно это знание даёт ему основания не задумываться над проблемой умножения в столбик. Если бы он не доверял алгоритму, неважно было бы, кто бы собственно выполнял алгоритм - он сам в уме, он сам на бумаге или компьютерная программа - результату он бы всё равно не поверил.
Теперь становится понятней, что упускают А и Б, и в чём упущение "формального аргумента". Все выдвигаемые возражения против компьютера относятся ко второй, физической фазе.
Все эти "вероятностные электроны" и "ошибки CPU" - детали физического воплощения. Стоит ли "доверять" им? Это всё ещё нетривиальный вопрос, но стандартный ответ на него теперь приобретает несколько большую силу. Стандартный ответ таков: мы можем повторить вычисление тысячи раз и проверить, что получаем один и тот же результат. "Железо" сбоит? Так мы запустим его на десятках разных компьютеров разных архитектур. Компилятор может содержать ошибку? Перепишем алгоритм на десятке других языков программирования и пропустим через десять других компиляторов.
Мы можем объективно оценить вероятность "сбоя" компьютера/компилятора/экрана/проводки и путём независимых повторов такого рода сделать её сколь угодно малой. Сколь угодно, но не нулём - возражает А! Что ж, он прав. Но когда эта вероятность становится ниже вероятности спонтанного превращение Солнца в суперновую звезду в ближайшие пять минут, например, это кажется не столь уж важным. Особенно учитывая первую, математическую фазу доверия, о которой А до сих пор не задумался.
Закончить сегодня у меня шансов нет, поэтому подытожу. Итак, какова моя позиция? Психологические проблемы математика А проистекают от реальных философских проблем, но он неправильно идентифицирует эти проблемы: вместо того, чтобы заняться алгоритмом, он занимается его физическим воплощением. Вероятность физической ошибки может быть сделана сколь угодно малой, намного меньше, чем вероятность ошибки самого А при перемножении чисел в столбик; А понимает это "умом", но не "сердцем" именно потому, что сознание этого факта не успокаивает его интуицию, не отметает психологическую проблему. А заключает, что даже абсурдно малая вероятность мешает ему; на самом деле ему мешают проблемы с первой фазой доверия, математически-абстрактной, но он этого не осознаёт.
Каковы же эти проблемы? Доверяем же мы, действительно, алгоритму умножения в столбик! Почему бы не доверять алгоритму, который помогает нам доказать теорему четырёх цветов? Об этом - в следующей записи, уже утром.
french_man подробно описал своё (положительное) отношение к использованию компьютерных программ в математических доказательствах здесь (два коммента), за что ему большое спасибо. Я опрометчиво пообещал сделать то же самое: пришлось основательно подумать, чтобы понять, какова же собственно моя позиция по этому поводу. Надумалось довольно много. Итак, речь идёт о математических теоремах (или, более обще и неопределённо, результатах), в процессе доказательства (получения) которых нетривиальным образом используются компьютерные программы. Уточним: речь идёт о теоремах в "чистой" математике, не требующих априори длинных вычислений (в конце концов, "найдите первый миллион цифр в десятичном разложении пи" тоже ведь математическая задача). Более важно уточнить, что значит "нетривиальным образом": это значит, что заменить запуск программы ручной проверкой не представляется возможным (скажем, такая проверка заняла бы миллион лет).
Канонический пример - знаменитая теорема о раскраске карты в четыре цвета. Дана карта неких областей, скажем, государств, с произвольным размером областей и их количеством. Всегда ли можно раскрасить эту карту, закрашивая каждую область полностью одним цветом, так, чтобы две смежные области всегда были разного цвета, и используя всего 4 цвета?
Все известные доказательства этой теоремы используют компьютерные программы нетривиальным образом. Впервые её доказали Аппель и Хакен в 1976-м году, а недавно было опубликовано новое, более простое доказательство. В обоих случаях доказательство состоит из теоретической части, в которой доказываются некоторые свойства, которыми обязан обладать контрпример, опровергающий теорему (а именно: он должен содержать в себе конфигурацию специального вида, и всего таких возможных конфигураций конечное количество), и компьютерной части, в которой вполне нетривиальный алгоритм перебирает это конечное кол-во конфигураций и проверяет, что ни одна из них не "подходит" для включения в контрпример (я здесь немного упростил, но несущественно).
О доказательствах такого рода можно задать два вопроса:
1. Насколько стоит им доверять? Должны ли они иметь такой же статус, как "обычные" доказательства? Каковы аргументы за или против использования таких доказательств?
Это вопрос философский, относящийся к философии математики.
2. Как к ним в действительности относятся в математическом сообществе? Как к ним относятся математики и какие аргументы выдвигают в поддержку своих мнений?
Это вопрос социологический.
На самом деле, эти два вопроса, конечно же, тесно связаны, и вообще не очень получается думать о них по отдельности. Но я попытаюсь обосновать следующую гипотезу: предлагаемые математиками причины неприятия таких доказательств обычно неубедительны, но, возможно, за чувствами неудобства, неприятия, неуютности, испытываемыми математиками, скрываются другие объективные причины, которыми они сознательно не оперируют и потому не предлагают в качестве объяснений.
french_man предлагает следующий достаточно убедительный список выдвигаемых обычно причин "против" - а) Формальные: Нет абсолютной точности, т.к. она недостижима в физическом мире (компьютеры ломаются, электроны управляются вероятностями).
б) Концептуальные: Такие доказательства "механичны", не добавляют ничего к нашему пониманию математики.
в) Психологические: неуютно.
- и отвергает их одну за другой. С его возражениями я в принципе согласен, и согласен с тем, что это причины обычно выдвигаемые (вопрос номер 2 выше), но не согласен с тем, что это все возможные причины "быть против" (вопрос номер 1 выше). К особо интересующему меня аргументу можно придти только путём пристального анализа этих, уже выдвинутых, причин.
"Концептуальный" аргумент меня не очень интересует, и принципиальным, на мой взгляд, не является. Не буду на нём останавливаться. "Психологический" аргумент сам по себе аргументом не является - это констатация факта. Математикам "не нравятся" такие доказательства, им неуютно с ними. Но почему не нравятся? - это нужно пытаться объяснить отдельно. Остаётся "формальный" аргумент, кстати, по моему опыту, как раз наиболее часто встречающийся.
А: Я не доверяю компьютеру. Компьютеры ошибаются.
Б: В каком смысле ошибаются?
А: В прямом. Как может моя вера в правильность доказательства зависеть от того, что какая-то там проволока правильно соединилась с другой проволокой и не соскочила?
Б: Но ведь математики тоже ошибаются. Причём постоянно и, пожалуй, куда чаще компьютеров.
А: Ну это потому что они и задачи выполняют куда сложнее компьютерных! И вообще, это другое.
Б: Но почему другое?
А: Не знаю. Но чувствую. Может быть, вот почему: математик сам отвечает за свои ошибки. Это его проблемы, и в идеале, если он постарается, он их обнаружит.
Б: Посадим параллельно компьютер и математика перемножать много 200-значных чисел. Кто больше раз ошибётся? Ответ очевиден. В конце концов, просто с прагматической точки зрения стоит доверять компьютеру. А чувства-шмувства... это просто от привычки. Привыкнем доверять компьютерам - и интуиция изменится.
В этом диалоге А - некий общий образ математика, настроенного "против" компьютерных доказательств, а Б - математика, настроенного "за", и использующего примерно те же аргументы, что высказал
french_man. Оба математика, однако, упускают одну важную деталь. Какую?Мы доверяем не компьютеру, а алгоритму.
Эту мысль надо пояснить. Более строго скажем так: нашу веру (или неверие) в то, что компьютер выдаёт правильный результат после решения поставленной перед ним задачи, можно (и нужно, непременно нужно!) разбить на две части:
1. Мы доверяем алгоритму, составленному для решения задачи. Это значит, что мы верим в то, что алгоритм действительно правильно её решает. Алгоритм - математический объект.
2. Мы доверяем инженерам, сконструировавшим компьютер. Это значит, что мы верим в то, что компьютер безошибочно выполняет алгоритм. Компьютер - физическое устройство.
Первая составляющая нашего доверия - исключительно математическая, абстрактная. Вторая составляющая - исключительно физическая, прагматическая.
Давайте убедимся в том, что первая составляющая действительно существует и реальна. Вопрос: почему математик не боится умножать в столбик? Ведь умножение в столбик - это тоже алгоритм, во время выполнения которого думать не надо, а надо глупо следовать правилам. Ответ: потому что математик доверяет алгоритму. Он знает (и может строго доказать), что если взять число X и число Y, и провести с их десятичными представлениями некоторое количество странных сложений, сдвигов и переносов "в уме", то получится десятичное представление числа X*Y. Именно это знание даёт ему основания не задумываться над проблемой умножения в столбик. Если бы он не доверял алгоритму, неважно было бы, кто бы собственно выполнял алгоритм - он сам в уме, он сам на бумаге или компьютерная программа - результату он бы всё равно не поверил.
Теперь становится понятней, что упускают А и Б, и в чём упущение "формального аргумента". Все выдвигаемые возражения против компьютера относятся ко второй, физической фазе.
Все эти "вероятностные электроны" и "ошибки CPU" - детали физического воплощения. Стоит ли "доверять" им? Это всё ещё нетривиальный вопрос, но стандартный ответ на него теперь приобретает несколько большую силу. Стандартный ответ таков: мы можем повторить вычисление тысячи раз и проверить, что получаем один и тот же результат. "Железо" сбоит? Так мы запустим его на десятках разных компьютеров разных архитектур. Компилятор может содержать ошибку? Перепишем алгоритм на десятке других языков программирования и пропустим через десять других компиляторов.
Мы можем объективно оценить вероятность "сбоя" компьютера/компилятора/экрана/проводки и путём независимых повторов такого рода сделать её сколь угодно малой. Сколь угодно, но не нулём - возражает А! Что ж, он прав. Но когда эта вероятность становится ниже вероятности спонтанного превращение Солнца в суперновую звезду в ближайшие пять минут, например, это кажется не столь уж важным. Особенно учитывая первую, математическую фазу доверия, о которой А до сих пор не задумался.
Закончить сегодня у меня шансов нет, поэтому подытожу. Итак, какова моя позиция? Психологические проблемы математика А проистекают от реальных философских проблем, но он неправильно идентифицирует эти проблемы: вместо того, чтобы заняться алгоритмом, он занимается его физическим воплощением. Вероятность физической ошибки может быть сделана сколь угодно малой, намного меньше, чем вероятность ошибки самого А при перемножении чисел в столбик; А понимает это "умом", но не "сердцем" именно потому, что сознание этого факта не успокаивает его интуицию, не отметает психологическую проблему. А заключает, что даже абсурдно малая вероятность мешает ему; на самом деле ему мешают проблемы с первой фазой доверия, математически-абстрактной, но он этого не осознаёт.
Каковы же эти проблемы? Доверяем же мы, действительно, алгоритму умножения в столбик! Почему бы не доверять алгоритму, который помогает нам доказать теорему четырёх цветов? Об этом - в следующей записи, уже утром.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
Ñîîáðàæåíèÿ ðåëèãèîçíîãî õàðàêòåðà
Date: 2001-09-10 02:05 am (UTC)íî ìîãó ñâèäåòåëüñòâîâàòü, ÷òî À. Ãðîòåíäèê èìåë
ñîîáðàæåíèÿ ðåëèãèîçíîãî õàðàêòåðà. Âèäèìî, èõ
ñëåäóåò ïåðåäàâàòü ïðèìåðíî òàê
1) Âñå, ÷òî åñòü ðåàëüíîãî â ìèðå ìàòåìàòè÷åñêèõ îáúåêòîâ,
ïðè íàäëåæàùåì êîíòàêòå ñàìî ñîîáùàåò íàèëó÷øèé ñïîñîá ñâîåãî
îïèñàíèÿ. Äî òåõ ïîð, ïîêà òîò èëè èíîé ôàêò íå ñîçðåë,
åãî áåññìûñëåííî òÿíóòü êëåùàìè. Ìîæíî âûòÿíóòü, íî
ýòî íå ïðèíåñåò ÿñíîñòè.
2) Íå òîëüêî êîìïüþòåðíûå (êàê óæå ãîâîðèëîñü), íî è
îáûêíîâåííûå ìàòåìàòè÷åñêèå äîêàçàòåëüñòâà, êîãäà îíè
çàíèìàþò ñîðîê ñòðàíèö çàôîðìóëåííîãî òåêñòà, íå÷èòàáåëüíû.
Ïðîâåðèòü, åñòü ëè â íèõ îøèáêà, íà ñàìîì äåëå íåâîçìîæíî.
(Ãðîòåíäèê ïðèâîäèò ïðèìåðû, êîãäà ýòî íè ó êîãî íå
ïîëó÷àëîñü, ñðåäè íèõ êîìïüþòåðíîå -- âïðî÷åì, åùå â åãî
âðåìåíà îêàçàâøååñÿ îøèáî÷íûì -- "äîêàçàòåëüñòâî" ïðîáëåìû
÷åòûðåõ êðàñîê.) Ãîâîðÿ î äîêàçàòåëüñòâàõ, ñëåäóåò èìåòü
â âèäó íå òîëüêî ôîðìàëüíóþ âîçìîæíîñòü ïðîâåðèòü
àêêóðàòíîñòü ïîñòðîåíèé -- îíà óæå äàåò ñáîè -- íî
"åñòåñòâåííîñòü" äîêàçàòåëüñòâà: êîãäà ïðîáëåìà ïîíÿòà
âïîëíå è âçÿòà îòòóäà, ãäå îíà äåéñòâèòåëüíî ëåæèò,
äîêàçàòåëüñòâî òèïà ñàìî ïîä íîãè ïàäàåò.
Òàêèå ñîîáðàæåíèÿ À. Ãðîòåíäèêà è âîîáùå äåëà.
Þëÿ.