Брайан Дэвис (фото с сайта www.mth.kcl.ac.uk)

Статья опубликована в журнале Notices of the American Mathematical Society, декабрь 2005, vol. 52, №11.

Оригинал статьи (PDF, 447 Кбайт).

Публикуется на русском языке впервые — с любезного разрешения автора и редакции журнала.

Редакция «Элементов» благодарит профессора математики Юрия Сафарова за ценные замечания по русскому переводу статьи.

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

Автор выражает благодарность М. Ашбахеру и С. А. Р. Хоару за ценные советы.

1. Введение
   
2. Доказательства с использованием компьютера
   
3. Формальная проверка доказательств
   
4. Простые конечные группы
   
5. Непротиворечивость арифметики
   
6. Обсуждение
   
7. Ссылки

^

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

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

Внешний консенсус среди математиков, как представителей математики, лишь дополнительно оттеняет вопиющие разногласия между исследователями философии математики. Главные споры здесь ведутся вокруг одного предмета, а именно — особого статуса математических объектов: если принять их существующими в некоем абстрактном платоновском мире, то непонятно, как можем мы, существа, живущие в реальном пространстве и времени, что-либо о них узнать. Довод, что, даже не имея прямого доступа к этим объектам, мы тем не менее можем силой логического разума приходить к определенным заключениям относительно них, неубедителен по следующим (в частности) причинам: следуя всё той же логике рассуждений и исходя из тех же постулатов, мы пришли бы к абсолютно тем же построениям и заключениям относительно свойств и связей между математическими объектами и в том случае, если бы платоновского мира, в котором они пребывают, вовсе не существовало. Взаимосвязи между онтологией и эпистемологией математики посвящены целые тома, однако справедливости ради остается лишь признать, что до согласия по этому вопросу пока далеко [5], [6], [25], [26].

Математики как философы-любители в отношении определения реального статуса предмета своей науки ушли не дальше философов-профессионалов. В качестве представителей многочисленных сторонников основных концепций назовем Роджера Пенроуза как реалиста (т. е. последователя Платона) [20], [21] и Пола Коэна как убежденного сторонника абстрактной концепции [12], [13]. Эйнштейн четко сформулировал свою позицию, заявив, что математика — продукт человеческого мышления, и поэтому даже самые убедительные математические выкладки и доказательства к реальному миру отношения не имеют [16]. Автор настоящей статьи в свое время также критиковал позицию последователей Платона [14]; сегодня же он полностью признает объективное существование математических величин, но лишь в карнапиевой интерпретации [15]. Согласно этой трактовке математические теории, возможно, и являются плодом человеческого воображения, однако при этом имеют строго определенные свойства — подобно правилам шахматной игры или римскому праву; аналогичным образом допускается и существование чисел — подобно существованию шахматных фигур. Хорошо еще, что математики, выступая в роли математиков как таковых, могут отбросить в сторону свои философские воззрения и благодаря этому во многом приходят к согласию. Но и в математической науке полного единодушия не наблюдается: конструктивисты признают лишь строгое, алгоритмически доказуемое понятие существования, которое более приемлемо с точки зрения прикладной математики, математического анализа, теории числовых методов и математической логики, нежели с точки зрения «чистой» абстрактной математики [7], [8], [9], [15].

Поразительные прозрения Курта Гёделя в 1930-е годы привели к первому из трех кризисов, о которых идет речь. Он продемонстрировал, что в рамках любой достаточно богатой системы аксиом, найдутся утверждения, которые невозможно ни доказать, ни опровергнуть. Он же установил недоказуемость непротиворечивости арифметики. Работы Гёделя широко обсуждались, однако часто с позиций явных или неявных субъективных философских предпосылок авторов такой критики. Например, вера самого Гёделя в то, что континуум-гипотеза либо истинна, либо ложна, вне зависимости от нашей способности доказать или опровергнуть ее, выдает в нем искреннего приверженца платоновской идеи в математике. Теоремы Гёделя носят чисто технический характер и не проводят принципиальной границы между истиной и доказуемостью в чисто математическом понимании, без привнесения элемента внешних философских предпосылок.

Можно было бы заподозрить Гёделя в чрезмерно высокой оценке полученных им результатов, если бы не эксцентричный характер самого ученого. В частности, его убеждение, что математическая интуиция по объективности восприятия не уступает органам чувств, явно противоречит единодушному мнению физиологов и психологов, согласно которому чувственное восприятие в значительной мере зависит от внутреннего устройства головного мозга человека [11], [14, с. 38]. У других гигантов математической логики отношение к своему предмету совсем иное. Например, Пол Коэн, обосновавший недоказуемость континуум-гипотезы, вовсе не разделял взглядов Гёделя и полагал, что теория множеств — не более чем аксиоматическая структура, а отнюдь не частная модель внешнего мира [12], [13].

При всём огромном объеме литературы, подчеркивающей важность работы Гёделя для понимания оснований и философии математики, на самих математиков (кроме специалистов в области логики, рассматриваемой как один из многих разделов математики) теоремы Гёделя долгие десятилетия практически никакого впечатления не производили. Ее прямая связь с основным руслом математической мысли вскрылась лишь когда было обнаружено, что проблема тождества слов и проблема изоморфизма групп с конечным представлением неразрешимы алгоритмическими методами и, как следствие, алгоритмически неразрешима задача о гомеоморфизме четырехмерных многообразий. Чем дальше, тем больше возникало такого рода проблем, однако большинство математиков с завидным упорством продолжало вспахивать свою ниву так, будто никакого Гёделя на свете не существовало.

Однако с 1970-х годов в математике произошли еще два кризиса — и оба столь же непредсказуемые, как и кризис, вызванный работой Гёделя. Оба они связаны с проблемой переусложненности: доказательства стали настолько длинными и сложными, что ни один ученый не взял бы на себя смелость однозначно подтвердить или оспорить их правильность. Эти кризисы в философской литературе широко не обсуждались, хотя как раз они сказались на математическом мышлении и отношении математиков к своей науке значительно серьезнее, чем кризис, вызванный теоремами Гёделя. В октябре 2004 года Королевское общество провело в Лондоне двухдневную дискуссию на тему «Природа математического доказательства», посвященную возможным путям выхода из вышеназванных кризисов [10]. Дискуссия выявила широкий спектр мнений по этому вопросу — и ни одного приемлемого решения. Налицо была проблема серьезного взаимного непонимания между математиками и кибернетиками.

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

^

Первым примером крупной математической теоремы, для доказательства которой был применен компьютер, стала теорема о четырех цветах, доказанная в 1976 году Аппелом и Хакеном [1], [2]. Это сильно обеспокоило многих математиков по двум причинам. Во-первых, был выдвинут довод, что в корректности доказательства невозможно убедиться, не перепроверив вручную все итерации расчетов, проделанных машиной. На тот момент доказательства «правильных» теорем еще казались практически всем математикам безупречными. Возможность случайных ошибок в доказательствах признавалась, но их исправление считалось делом времени. Другое дело, что уже тогда некоторые математики стали задумываться не над тем, истинна ли та или иная теорема, а над тем, почему она считается истинной. Доказательства без понимания сути их не интересовали.

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

Задача Кеплера заключается в поиске наиболее компактного варианта упорядочивания твердых сферических тел равного диаметра в трехмерном объеме с целью получить максимальную среднюю плотность его заполнения. Ожидаемое решение известно уже давно и широко практикуется на прилавках с апельсинами, выложенными горкой. В 1998 году Том Хейлз объявил о найденном им строгом математическом решении задачи Кеплера, основанном на сочетание аналитической геометрии и сложных компьютерных вычислений. Журнал «Анналы математики» принял статью на экспертизу и созвал комиссию из двадцати ведущих специалистов в этой области, чтобы они дали отзыв о статье. Экспертная комиссия начала свою работу с конференции в Принстонском университете по выработке общей стратегии. Шли годы, референты постепенно выходили из состава комиссии, и наконец в начале 2004 года было окончательно решено отказаться от усилий рецензировать статью. Редколлегия журнала решила опубликовать «теоретическую часть» работы, а «компьютерную часть» переадресовать в какой-нибудь более подходящий журнал. Член редколлегии «Анналов» Роберт Макферсон по этому случаю заметил, что «в отношении статей подобного рода (негласные) редакционные правила отбора материалов к публикации просто не работают» [18].

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

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

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

Из положительных сторон я должен все-таки отметить, что компьютеры значительно разгрузили чистых математиков от нудных рутинных расчетов. Вот лишь несколько наугад взятых примеров, которые можно подразделить на несколько категорий. Компьютерная алгебра позволяет быстро производить безнадежно долгие в иных случаях вычисления, необходимые во многих областях знания. Статистическая физика, изучающая динамику поведения макросистем, состоящих из огромного набора хаотически движущихся частиц, не могла бы достичь современного уровня развития без возможности проведения колоссального количества числовых экспериментов. Да, верно, неупорядоченный характер движения тепловых частиц был открыт Анри Пуанкаре еще в конце XIX века; но так же верно и то, что прогрессом статистической физики мы во многом обязаны развитию компьютерных технологий. Невероятная разница в спектральных характеристиках самосопряженных и несамосопряженных матриц была выявлена именно благодаря численным методам и привела к развитию совершенно новой области псевдоспектрального анализа, который сегодня справедливо считается самостоятельным и полноправным разделом «строгой математики» [28].

Контролируемые численные методы сегодня играют важнейшую роль и в статьях, посвященных проблемам чистой математики. В некоторых областях, в частности в области нелинейных дифференциальных уравнений высокого порядка, только компьютерные методы позволили доказать существование решений [22], [23]. При этом в расчетах использовались стандартные итерационные методы и методики расчета допустимых ошибок и доверительных интервалов, принципиальную правильность которых сегодня никто не оспаривает. Главное — строгое доказательство неравенства, которое затем становится неотъемлемой частью доказательства теоремы. В принципе, все те же расчеты можно было бы проделать и вручную, только вот на практике такие трудозатраты оказываются нереальными.

^

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

Формальная проверка корректности работы программного обеспечения — забота одновременно и специалистов в области прикладной математической логики, и представителей бизнеса. В частности, повышение надежности Windows XP было достигнуто благодаря мощному аппарату анализа корректности программного обеспечения, который основан на математических методах формальной проверки непротиворечивости математических же алгоритмов, лежащих в основе функционирования программ. Однако в некоторых отношениях проблемы кибернетики и математики лежат в принципиально различных плоскостях. Техническая документация некоторых языков программирования, таких как Java, может занимать сотни страниц — значительно больше, чем может потребоваться для формулировки самой заумной теоремы. Иногда трудно даже сказать, «своеобразное» поведение программного обеспечения — это ошибка или особенность программы. Зависания (часто вследствие переполнения буфера) — это, несомненно, недоработки программистов; сложнее сказать что-либо определенное, когда LATEX, например, отказывается делать по запросу пользователя что-то такое, о чем разработчикам не пришло в голову, что такая функция вообще может кому-нибудь понадобиться. Вообще, неадекватные технические задания на разработку крупных программных пакетов — гораздо более распространенная причина катастрофических сбоев с непредсказуемыми экономическими последствиями, нежели неправильное выполнение технических заданий программистами.

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

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

Нередко при обосновании какого-либо шага доказательства автор ссылается на некие классические результаты, не давая ссылок на первоисточник. Недавно один мой студент поймал меня на некорректном применении теоремы Мерсера. Формулировка самого Мерсера оперирует ядром на одномерном интервале, я же использовал более общую формулировку, причем безо всяких объяснений. Когда студент попросил меня обосновать мою версию, я не смог найти в литературе формулировки теоремы достаточно общей, чтобы охватить и использованную мной трактовку. Пролистав с полдюжины книг, я решил сам написать это доказательство. Любому человеку, подобно мне, знакомому с исходным доказательством для линейного интервала, возможность его перенесения на случай с конечным числом измерений должна быть очевидна, однако на строгое доказательство теоремы в общей форме у меня ушло четыре страницы. При этом серьезной педагогической ошибки я, по-моему, не допустил, поскольку доказуемость требуемого результата в данном случае была очевидна, оставалось лишь кропотливо перенести все смысловые этапы доказательства Мерсера с одномерного случая на многомерный. В конце концов студента мое доказательство удовлетворило.

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

^

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

В 1970-е годы более сотни специалистов по теории групп образовали своеобразный консорциум, целью которого было представить полную классификацию простых конечных групп. Задача была поставлена крайне трудоемкая, и ее решение остается единственным примером использования «поточного метода» и «разделения труда» в чистой математике. Под общим руководством Даниэля Горенштейна проблема была разбита на «пакеты» задач, которые поручили различным группам математиков всего мира. Через десять лет интенсивной работы удалось составить полную классификацию всех простых конечных групп, состоящую из трех бесконечных счетных семейств и 26 так называемых спорадических групп с особыми свойствами. Существование спорадической группы с самым большим порядком, получившей прозвище «монстр», удалось доказать только при помощи компьютера. К счастью, кризис, разразившийся вокруг этой проблемы, можно обсуждать не вникая в детали классификации групп. Не обязательно даже вообще знать, что такое простая конечная группа.

В 1980-е годы случилось нечто не менее интересное, чем сама классификация групп. Сначала произошел внешне позитивный сдвиг: вроде бы удалось найти метод доказательства существования «монстра» без использования компьютера. Было решено объединить усилия различных групп математиков для проведения массированной проработки нащупанного доказательства, но вместо ожидаемого результата было выявлено множество пробелов в ранее принятых доказательствах. Большую часть дыр удалось залатать, но одна оказалась настолько серьезной, что заявления о том, что получена полная классификация простых конечных групп, были в 1990 году признаны преждевременными. Со временем этот пробел был заполнен доказательством Ашбахера и Смита, и опять тогда казалось, что доказательство вполне корректно [3]. Интересно, что из двадцати томов этого окончательного доказательства до сих опубликованы лишь неполные пять, и это спустя четверть века после того, как теорема была «доказана»; подробнее см. [3], [27]. Михаэль Ашбахер, один из самых заинтересованных участников проекта, не исключает, что в один прекрасный день может быть открыта новая простая конечная группа. Если ее характеристики окажутся родственными характеристикам какой-либо из известных групп, это еще не страшно. Однако Ашбахер не исключает и возможности открытия принципиально новой простой конечной группы, и тогда всю работу по их классификации можно начинать заново; см. [4]. Отметим также, что и Жан-Пьер Серр весьма скептически относится к полноте и корректности имеющегося доказательства [24].

Ашбахер считает доказательство «внешне достаточно крепким». Под этим он подразумевает, что выявленные недостатки пока что удавалось исправлять за счет умеренных объемов дополнительной работы, не затрагивая основной линии доказательства. К сожалению, это не означает, что доказательство корректно. Сила любого доказательства определяется слабейшим из его звеньев, и тот факт, что до сегодняшнего дня выпадавшие звенья удавалось относительно безболезненно заменять новыми, не гарантирует, что это будет раз за разом удаваться и в дальнейшем. Если представить себе такое доказательство в виде сети, в которой разрыв отдельных нитей не угрожает целостности всей сети, то нельзя исключить, что где-то в этой сети осталась дыра, достаточно большая для того, чтобы муха смогла через нее проползти. Подавляющее большинство мух (в нашем случае — простых конечных групп) поймано, но не обязательно все.

Сама идея сравнения математических знаний с паутиной взаимосвязанных фактов снижает роль линейной логики и переводит вопрос математического доказательства в вероятностную плоскость, что неизбежно ведет к излишней структурной сложности. Эта идея не нова, но сами математики обратились к ней сравнительно недавно. Подобную аналогию приводит, в частности, Ашбахер [4], проводя параллель между современной математикой и биологией как информационно емкой наукой, изобилующей различными способами организации данных, по контрасту с «классической математикой».

Что касается завершения проекта окончательной классификации конечных групп (в смысле публикации исчерпывающего итогового доклада), то оно находится под угрозой срыва в связи с выбытием из строя ведущих участников в силу естественных возрастных причин. Еще лет десять, и большинство из них уйдет из жизни или из математики, и останется слишком мало ученых, достаточно глубоко понимающих проблему, чтобы завершить классификацию. Но даже если проект увенчается исчерпывающим итоговым докладом, в мире, наверное, не найдется и десяти математиков, которые будут вправе утверждать, что они понимают хотя бы основные линии многотомного доказательства.

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

Не исключено, конечно, что в один прекрасный день найдется более простой подход к решению проблемы классификации групп; но точно так же не исключено, что этого не произойдет. Ашбахер скептически относится к возможности существования относительно простого доказательства, учитывая тот факт, что оцениваемая общая длина (всё еще не записанного) имеющегося доказательства за прошедшие четверть века нисколько не сократилась. Из работы Тьюринга следует, что существуют теоремы, доказательство которых во много раз длиннее их формулировки: фактически, соотношение этих двух длин может быть произвольно большим. Коэн считает, что «подавляющее большинство даже элементарных вопросов теории чисел средней сложности выходят за рамки разумного понимания» [13]. Так что в будущем приходится ожидать лишь новых открытий подобного рода.

^

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

Платоновские настроения, царящие в среде математиков, просто не дают им усомниться в безгрешности арифметики Пеано. Вслед за Кронекером многие стали считать, что натуральные числа открыты им путем прямого прозрения и, следовательно, существуют. А раз натуральные числа существуют и подчиняются аксиомам Пеано, следовательно аксиоматика Пеано есть данность, и ее надо считать априори непротиворечивой. При этом часто ссылаются на ожидаемые или замышляемые улучшенные модели аксиом Пеано, однако ожидания и замыслы сами по себе ничего не решают.

Если мы обратимся к истории, мы увидим множество примеров всеобщей уверенности в ошибочных постулатах, включая математические. Веками евклидова геометрия считалась адекватно описывающей свойства пространства, пока Риман, а затем Эйнштейн не доказали обратное. Статус аксиомы выбора, или аксиомы Цермело, сегодня ни у кого сомнений не вызывает, хотя в начале XX века ее приемлемость была предметом бурных споров. Сам Цермело со временем признал, что главная причина для принятия аксиомы выбора — это то, что без нее математики не смогли бы доказать целый ряд результатов, необходимых им в работе; см. [19, с. 56]. И все эти сомнения отнюдь не разрешены — они просто забыты большинством научного сообщества. Наконец, отметим, что уверенность Гильберта в возможности позитивного решения всех без исключения математических задач разделялась подавляющим большинством его современников и была поколеблена лишь Гёделем.

А ведь логически не исключена возможность того, что арифметика Пеано внутренне противоречива. Никаких свидетельств в пользу этого нет, и я вовсе не утверждаю, что вероятность этого высока — и всё же такая возможность сохраняется. Чтобы разобраться с этим, рассмотрим пример из теории групп. Возьмем следующий набор аксиом:

(1) Существует множество элементов G, подчиняющееся аксиомам группы.

(2) Группа G конечна, но не изоморфна никаким из известных простых конечных групп.

(3) Группа G — простая. Иными словами, если N — подмножество G с определенным набором свойств (со свойствами нормальной невырожденной подгруппы), то N = G.

Эти аксиомы можно сравнить с арифметикой Пеано. Третья аксиома аналогична по форме аксиоме индукции (или схеме аксиом в логике первого порядка) в том плане, что, взяв произвольный объект с определенными свойствами, она признает его равным G (при этом мы допускаем свободный переход туда и обратно между подмножествами и предикатами). Хотя мы полагаем группу G конечной, ее размер не задан, и значит нельзя просто перечислить все объекты этого типа, даже если на это будет отведено бесконечно много времени. Единственный способ понять работу этой системы аксиом — через доказательства на ее основе.

Тот факт, что аксиоматика, столь близкая к арифметике Пеано, может потребовать столь длинного доказательства своей противоречивости (если она действительно противоречива, как полагают многие специалисты по теории групп), заставляет усомниться и в непротиворечивости самой арифметики Пеано. Самое короткое доказательство противоречивости аксиом Пеано может занимать миллиард страниц, и мы никогда его не увидим. А раз мы никогда не столкнемся с противоречием, то какая нам разница, противоречива аксиоматика или нет? Мы можем и дальше доказывать теоремы и вскрывать интересные взаимосвязи между понятиями, даже не подозревая об ужасной истине!

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

^

Автору кажется, что решение задачи Кеплера имеет больше перспектив, нежели классификация простых конечных групп. Компьютерные программы когда-нибудь, возможно, будут переписаны таким образом, что удастся формально доказать корректность теоремы Хейлза. На заседаниях Королевского общества регулярно раздаются голоса математиков, повторяющих старый аргумент, что полученные результаты в любом случае будут неудовлетворительными, потому что программы дают сбой, компьютеры дают сбой и вообще не защищены от космических лучей. Всё это так, только наивно думать, будто вышеперечисленные факторы не распространяются на доказательства, созданные вручную человеком, свидетельством чему опыт классификации простых конечных групп. Единственное, что можно хотеть от компьютерных методов проверки доказательств, — это чтобы они делали свое дело лучше человека, то есть чтобы они находили ошибки, допущенные в доказательствах людьми, и чтобы люди с предъявленными ошибками соглашались. В области отладки программного обеспечения и проектирования микросхем это уже произошло, остается дождаться такого же отношения и от самих математиков.

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

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

В завершение зададимся вопросом, какие еще кризисы могут ждать математику в обозримом будущем. Одна из возможностей состоит во вскрытии внутреннего противоречия в математических рассуждениях такой сложности, о которой никто и помыслить не может. Можно попытаться представить себе противоречие в результате ошибки, заложенной на уровне глубже человеческого понимания или превышающем вычислительные возможности мощнейших компьютеров. Кто-то скажет, что до этого еще далеко, однако с компьютерными шахматными программами нечто подобное уже происходит: иногда они делают такие ходы, что никто из гроссмейстеров не находит им логического объяснения. Компьютер, конечно, обоснует любой свой ход тем, что из миллиардов рассмотренных комбинаций именно он с наибольшей вероятностью приводит к успеху в партии. Однако это не означает, что выбранный компьютером ход действительно лучший, поскольку варианты просчитывались по алгоритмам, заданным человеком. Если нечто подобное произойдет, нам останется лишь признать нашу ограниченность как биологического вида и очертить пределы возможностей нашего интеллекта — и не только в математике.

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

^


«Элементы»