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

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

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

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

Ответ на этот непростой вопрос заключается, возможно, в том, что доказательства постепенно переходят из разряда явлений индивидуального опыта в разряд явлений опыта коллективного. Тенденция к выдвижению на первый план коллективного вообще характерна для истории цивилизации. Хорошо известно (и подробно обсуждено), что с развитием человеческого общества возникают и неуклонно усиливаются разделение и кооперация труда. Лишь в глубокой древности человек мог сам, лично производить всё необходимое для себя; сейчас каждый вынужден пользоваться результатами труда других. Известно (хотя и не столь подробно обсуждено), что одновременно происходят разделение и кооперация научных знаний. Трудно сказать, когда – по-видимому, в Средние века – ещё находились отдельные учёные, способные охватить всю доступную их современникам сумму знаний. Сейчас каждый вынужден так или иначе использовать знания других. Аналогично обстоит дело и с доказательствами: деятельность в сфере производства и потребления доказательств стала в такой же степени объектом разделения и кооперации, как и деятельность в сфере производства и потребления знаний. Само понятие убедительности начинает терять свой индивидуализированный оттенок и всё больше приобретает коллективный характер. По-видимому, следует постепенно приучаться говорить об убедительности не для отдельного индивидуума, а для некоторого научного коллектива. При этом коллективная убедительность отнюдь не означает равную «непосредственную убедительность» для каждого в отдельности члена коллектива. Коллектив выступает не как простая сумма членов, а как единое целое. Смысл коллективной убедительности в том, что для каждой составной части доказательства найдётся свой «отвечающий за неё» член коллектива, для которого непосредственно убедительна именно эта часть (а другие члены коллектива полагаются в данном вопросе на этого члена).

Век информатики вносит свои коррективы и в представления о доказательствах. Возникают, например, случаи, когда доказательство требует перебора столь большого числа вариантов, что этот перебор делается недоступным человеку, а машине доступен. Допустим, машина перебрала все требуемые варианты и перебор привёл к нужным результатам. Можем ли мы считать, что получили доказательство? А что если машина дала так называемый сбой? (Но ведь и человек может ошибаться!) Кроме того, необходима гарантия, что сама программа (работы машины) составлена правильно; правильность программы требует особого доказательства, и теория таких доказательств образует специальный раздел теоретического программирования.

Реально компьютер был привлечён для решения проблемы четырёх красок. По простоте формулировки эта проблема, состоящая в доказательстве гипотезы четырёх красок, мало уступает проблеме Ферма (состоящей в доказательстве гипотезы Ферма), а по естественности постановки (и прикладному значению) её превосходит. Вот формулировка этой гипотезы в Большой Советской Энциклопедии (изд. 3-е, том 29, статья «Четырёх красок задача»): Четырёх различных красок достаточно для того, чтобы раскрасить любую карту так, чтобы никакие две области, имеющие общий участок границы, не были окрашены в один и тот же цвет. Проблема четырёх красок возникла в картографической среде: впервые наблюдение о достаточности четырёх красок было сделано в 1852 г. при составлении карты графств Англии. Обнаружилось, что гипотеза четырёх красок подтверждается во всех известных частных случаях. Сравнительно просто удаётся доказать (и это было сделано в 1890 г.), что для любой мыслимой карты достаточно пяти красок. Попытки же доказать аналогичное утверждение для четырёх красок долгое время (в течение ста лет) были безуспешны.

В 1976 г. Аппелем и Хакеном было анонсировано [17], а в 1977 г. изложено [18, 19] решение проблемы, основанное на сведéнии решения к большому числу частных случаев, рассмотрение которых можно поручить машине. Машина всё проверила, и таким образом было получено доказательство того, что всякую карту можно раскрасить четырьмя красками так, как нужно.

Казалось бы, проблема закрыта. Однако всё не так просто. Доказательство обладало двумя неприятными особенностями. Во-первых, рассуждения авторов были столь длинны и сложны, что никому не удавалось проверить их во всей полноте. Во-вторых, существенная часть доказательств состояла в использовании компьютера; именно компьютер, а не человек проверял, обладает ли каждая из почти двух тысяч специально отобранных карт некоторым требуемым качеством. Первая особенность была впоследствии устранена (если не полностью, то в очень большой степени) другими авторами, значительно упростившими первоначальные рассуждения Аппеля и Хакена. А вот избежать того, что в истинности большого числа фактов удостоверяется не человек, а компьютер, не удалось. А что