Ни о какой безапелляционности в моих высказываниях не может быть и речи!

Тема возникла в комментариях вот здесь. french_man подробно описал своё (положительное) отношение к использованию компьютерных программ в математических доказательствах здесь (два коммента), за что ему большое спасибо. Я опрометчиво пообещал сделать то же самое: пришлось основательно подумать, чтобы понять, какова же собственно моя позиция по этому поводу. Надумалось довольно много.

Итак, речь идёт о математических теоремах (или, более обще и неопределённо, результатах), в процессе доказательства (получения) которых нетривиальным образом используются компьютерные программы. Уточним: речь идёт о теоремах в "чистой" математике, не требующих априори длинных вычислений (в конце концов, "найдите первый миллион цифр в десятичном разложении пи" тоже ведь математическая задача). Более важно уточнить, что значит "нетривиальным образом": это значит, что заменить запуск программы ручной проверкой не представляется возможным (скажем, такая проверка заняла бы миллион лет).

Канонический пример - знаменитая теорема о раскраске карты в четыре цвета. Дана карта неких областей, скажем, государств, с произвольным размером областей и их количеством. Всегда ли можно раскрасить эту карту, закрашивая каждую область полностью одним цветом, так, чтобы две смежные области всегда были разного цвета, и используя всего 4 цвета?
( Collapse )

Продолжение вот этой записи.

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

Представим себе математика М, который не знает об этом баге, и который решил проверить, не забыл ли он ещё, как делят в столбик числа без компьютера. ( Collapse )

Следует за частями первой и второй.

Постараюсь, наконец, увязать всё это вместе. Для этого мне нужно посмотреть внимательнее на то, что математики считают доказательством, а что не считают (не учитывая сейчас эти проблемы с компьютерами и программами). Чтобы немного сэкономить время и место, я не буду подробно проводить разбор и обосновывать его, а вместо этого приведу собственно краткое описание своей точки зрения; если кто-то с ней не согласен, пожалуйста оспорьте:

---

Математическое доказательство на практике никогда не формально (не является формальным доказательством с точки зрения мат. логики), но всегда сохраняется принципиальная возможность относительно легко добиться абсолютной строгости. ( Collapse )