Стивен Кранц - Изменчивая природа математического доказательства. Доказать нельзя поверить

что еще меньше доказательств требуется для оправдания военных действий^[3]. Широкая панорама мнений о современном понятии доказательства — в самых разных контекстах — представлена в [NCBI]. Говорят (см. [MCI]), что в некоторых областях математики (таких как топология малой размерности) доказательство можно пересказать на языке жестов.

Французский математик Жан Лере (1906–1998) так пишет о системе ценностей в современной математике.

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

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

В доказательстве есть и человеческий фактор, который нельзя игнорировать. Принятие новой математической истины — это социологический процесс. Это что-то, что происходит в математическом сообществе. Оно включает понимание, усваивание, обдумывание и обсуждение. Самые выдающиеся математики иногда ошибаются и объявляют новые результаты, а потом выясняется, что неизвестно, как их доказать. В 1879 г. А. Кемпе опубликовал доказательство теоремы о четырех красках, и оно продержалось целых 11 лет, пока П. Хивуд не нашел фатальную ошибку в работе. Первая совместная работа Харди и Литтлвуда была заявлена на заседании Лондонского математического общества в июне 1911 г. Но она никогда не была опубликована, поскольку позднее они обнаружили ошибку в доказательстве. Коши, Ламе и Куммер — каждый из них в тот или иной момент своей карьеры полагал, что доказал Великую теорему Ферма. И каждый из них ошибался. Радемахер в 1945 г. думал, что опроверг гипотезу Римана. Его работа была даже опубликована в Time Magazine. Позднее Радемахеру пришлось отозвать свое утверждение, поскольку Зигель нашел ошибку. В этой книге мы изучаем социальную базу математических дисциплин, разбираемся, как во взаимодействии разных математиков и разных математических культур творится форма нашей науки. Математические ошибки исправляются, причем не формальной логикой, а другими математиками. Это один из краеугольных камней нашей науки^[4].

В самом начале XX в. Брауэр дал революционное доказательство своей теоремы о неподвижной точке, а спустя некоторое время решительно отрекся от доказательств от противного (по крайней мере в отношении доказательств существования, а результат о неподвижной точке был именно таким) и создал движение интуиционизма. Позднее эту программу поддержал Эррет Бишоп, и его работа Foundations of Constructive Analysis, написанная в 1967 г., была довольно заметной (переработанное издание, написанное в соавторстве с Дугласом Бриджесом, опубликовано в 1985 г.). Эти идеи представляют особенный интерес для специалистов в теории компьютерных наук, ведь значимость доказательств от противного в компьютерных науках небесспорна (несмотря даже на то, что в свое время Алан Тьюринг расшифровал код Энигмы, применив как раз идеи доказательства от противного в контексте вычислительных машин).

В последние тридцать лет или около того стало ясно, что мы переосмыслили и решительно расширили наше представление о доказательстве. В этом явлении важную динамичную роль сыграли компьютеры. Они могут делать сотни миллионов операций в секунду. Это открывает возможности для экспериментирования, вычисления и визуализации таких вещей, что были немыслимы полвека назад. Следует иметь в виду, что математическое мышление включает овладение понятиями и рассуждениями, в то время как компьютер — просто средство для манипулирования данными, это совершенно разные вещи. Непохоже (см. блестящую книгу Роджера Пенроуза «Новый ум короля»), что когда-либо компьютер сможет думать и доказывать математические теоремы так, как это делает человек. Тем не менее компьютер может предоставить ценную информацию и натолкнуть на идею. Он может изобразить для пользователя вещи, которые тот раньше --">