Профессор Брайан Дэвис, факультет математики Лондонского королевского колледжа (фото с сайта www.mth.kcl.ac.uk)

Американское математическое общество приняло к печати статью Брайана Дэвиса (Brian Davies), профессора Лондонского королевского колледжа. В работе, озаглавленной «Whither Mathematics?» («Куда идет математика?»), обосновывается, что в XX веке самая точная из точных наук испытала перелом, который принципиально меняет характер получаемых в ней результатов. В будущем, по мнению профессора Дэвиса, математика станет весьма значительно отличаться от той науки, что была известна на протяжении последних двух тысяч лет.

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

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

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

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

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

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

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

В качестве примера Дэвис приводит решение так называемой задачи Кеплера о наиболее плотной упаковке шаров. В 1998 году Томас Хейлс (Thomas Hales) представил в журнал Annals of Mathematics доказательство соответствующего утверждения, которое заняло более 250 листов и включало наряду с геометрическими рассуждениями результаты обширных компьютерных расчетов. Группа из двадцати экспертов, начавшая анализировать доказательство, окончательно распалась в 2004 году, так и не придя к окончательному заключению о правильности доказательства.

Но всё же в качестве подлинной кульминации «кошмара сложности» Брайан Дэвис приводит другой пример — проблему, известную под названием классификация простых конечных групп. Для обсуждаемого вопроса не так важно, в чем состоит сама эта проблема. Важно то, что теория групп лежит в основе многих направлений исследований в физике и математике, и поэтому вопрос о классификации групп считается весьма важным.

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

Для его решения в 1970-е годы был собран своего рода международный консорциум математиков. Около сотни теоретиков разделили между собой работу и приступили к решению проблемы. Это, по-видимому, единственный в истории пример подобного «промышленного» подхода к решению математической проблемы. Постепенно было выделено три бесконечных семейства групп и 26 особых случаев конечных групп (существование самой крупной из них удалось обнаружить только благодаря компьютерам).

После этого встал вопрос о доказательстве исчерпывающего характера этой классификации. Когда работы разных групп стали объединять в одно общее доказательство, стали обнаруживаться многочисленные пробелы. Большую часть из них постепенно удалось закрыть. Тем не менее на данный момент — спустя 25 лет после первого объявления о том, что теорема доказана, — опубликованы только 5 из 12 томов полного доказательства.

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

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

В заключении своей статьи Брайан Дэвис так описывает характер происходящих в математике изменений. «В 1875 году каждый человек, способный к математике, мог за несколько месяцев полностью разобраться в доказательстве большинства известных теорем. К 1975 году ... математики еще могли полностью понять доказательство любой доказанной теоремы. К 2075 году многие области чистой математики будут зависеть от теорем, которые не понимает никто из математиков — ни индивидуально, ни коллективно. ... Обычным делом станет формальная верификация сложных доказательств, но при этом будет много результатов, признание которых будет основано на социальном консенсусе в не меньшей мере, чем на строгом доказательстве».

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

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

Александр Сергеев
«Элементы»