Брайан Дэвис: «Куда идет математика?»

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

Первый из этих кризисов связан с теоремой Гёделя о неполноте, которая утверждает, что в любой достаточно богатой аксиоматической системе есть предложения, которые в ее рамках нельзя ни доказать, ни опровергнуть. Хотя теорема Гёделя оказала довольно незначительное влияние на практическую работу математиков, она самым непосредственным образом связана с проблемой онтологического статуса математических объектов.

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

Достаточно четырех цветов, чтобы раскрасить карту Великобритании так, что никакие два соседних графства не окрашены в один цвет. Так можно раскрасить любую карту на плоскости. Теорема была сформулирована в 1852 г. и доказана в 1976 г. с использованием компьютера (рис. из книги Саймона Сингха «Великая теорема Ферма», МЦНМО, 2000)

Второй кризис Брайан Дэвис связывает с вторжением в математику компьютеров. Рассматривая пример теоремы о раскрашивании карты четырьмя цветами, он напоминает, что полный перебор всех ветвей в доказательстве удалось выполнить только на компьютере. Однако у многих математиков возникает серьезное сомнение, насколько можно доверять подобным доказательствам, которые никогда не были полностью проверены «вручную».
Критика тут имеет несколько аспектов. Во-первых, компьютер мог дать сбой при вычислениях. Даже если результат проверен несколько раз, это лишь повышает вероятность правильности доказательства, но не сделает его абсолютно надежным. Во-вторых, в процессоре и вспомогательных программах (компиляторе, библиотеках и т. п.) могут содержаться (и даже наверняка содержатся) ошибки, и невозможно полностью исключить их влияние на правильность доказательства. И, наконец, самое главное: сама программа, которая была написана для поиска или проверки доказательства, тоже может содержать ошибки. Строго математически убедиться в том, что она в полной мере соответствует спецификации, настолько же сложно, как и проверить вручную выполненное с ее помощью доказательство (а возможно, и сложнее). Достаточно сказать, что описания языков, на которых пишутся программы, содержат сотни страниц не всегда идеально ясного текста. Включение таких описаний в формулировку теоремы лишает всяких перспектив на получение доказательства.
Все эти соображения привели к тому, что ряд чистых математиков крайне скептически относится к доказательствам, полученным с использованием компьютеров. И тем не менее в последние десятилетия появляется все больше теорем, доказательства которых совершенно необозримы для человеческого разума, если не усиливать его компьютером.

Томас Хейлс (Thomas Hales) из Мичиганского университета демонстрирует решение задачи Кеплера о наиболее плотной укладке шаров в пространстве, которая ждала своего решения с 1611 года (фото с сайта www.umich.edu)

В качестве примера Дэвис приводит решение так называемой задачи Кеплера о наиболее плотной упаковке шаров. В 1998 году Томас Хейлс (Thomas Hales) представил в журнал Annals of Mathematics доказательство соответствующего утверждения, которое заняло более 250 листов и включало наряду с геометрическими рассуждениями результаты обширных компьютерных расчетов. Группа из двадцати экспертов, начавшая анализировать доказательство, окончательно распалась в 2004 году, так и не придя к окончательному заключению о правильности доказательства.
Но всё же в качестве подлинной кульминации «кошмара сложности» Брайан Дэвис приводит другой пример — проблему, известную под названием классификация простых конечных групп. Для обсуждаемого вопроса не так важно, в чем состоит сама эта проблема. Важно то, что теория групп лежит в основе многих направлений исследований в физике и математике, и поэтому вопрос о классификации групп считается весьма важным.
Для его решения в 1970-е годы был собран своего рода международный консорциум математиков. Около сотни теоретиков разделили между собой работу и приступили к решению проблемы. Это, по-видимому, единственный в истории пример подобного «промышленного» подхода к решению математической проблемы. Постепенно было выделено три бесконечных семейства групп и 26 особых случаев конечных групп (существование самой крупной из них удалось обнаружить только благодаря компьютерам).
После этого встал вопрос о доказательстве исчерпывающего характера этой классификации. Когда работы разных групп стали объединять в одно общее доказательство, стали обнаруживаться многочисленные пробелы. Большую часть из них постепенно удалось закрыть. Тем не менее на данный момент — спустя 25 лет после первого объявления о том, что теорема доказана, — опубликованы только 5 из 12 томов полного доказательства.
По мнению специалистов, доказательство можно считать довольно устойчивым. Но это лишь означает, что известные на сегодня пробелы в доказательстве не выглядят принципиальными и, по-видимому, могут быть закрыты ценой умеренных усилий и без изменения общей стратегии доказательства. Тем не менее само наличие этих пробелов говорит о том, что нельзя дать гарантию надежности гигантского доказательства в целом. Но еще хуже то, что, даже если со временем все пробелы в доказательстве удастся закрыть, вряд ли на всей Земле найдется хотя бы десяток математиков, в достаточной мере понимающих логику монструозного доказательства.
Итак, математика столкнулась с проблемой практически непреодолимой сложности доказательств. Решение важной задачи, которая формулируется в нескольких предложениях, может занимать десятки тысяч страниц, что фактически делает невозможным его полную запись и понимание.
В заключении своей статьи Брайан Дэвис так описывает характер происходящих в математике изменений. «В 1875 году каждый человек, способный к математике, мог за несколько месяцев полностью разобраться в доказательстве большинства известных теорем. К 1975 году ... математики еще могли полностью понять доказательство любой доказанной теоремы. К 2075 году многие области чистой математики будут зависеть от теорем, которые не понимает никто из математиков — ни индивидуально, ни коллективно. ... Обычным делом станет формальная верификация сложных доказательств, но при этом будет много результатов, признание которых будет основано на социальном консенсусе в не меньшей мере, чем на строгом доказательстве».
Подобно инженерам, математики станут говорить не о твердом знании, а о степени уверенности в надежности своих результатов. Это может сблизить математику с другими дисциплинами и, возможно, приведет к снятию философского вопроса об особом онтологическом статусе математических объектов.

P.S. С полным текстом статьи можно ознакомиться здесь. На мой личный взгляд, она определенно заслуживает перевода на русский язык.

Александр Сергеев