"Экономика должна быть экономной!" - этот партийный лозунг 17-летней давности жизнь быстро укоротила до более актуального: "Экономика должна быть!" За последние 22 года компьютерной экспансии то же самое произошло со взглядами математиков на качества математического доказательства.

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

В 1976 году В.Хакен и К.Аппель доказали теорему о четырех красках. Наконец-то было найдено решение проблемы, не поддававшейся лучшим математическим умам в течение 124 лет. Но это вызвало не ликование математического мира, а негодование, неприязнь и осуждение. Парадокс? Все дело в том, какое доказательство предложили Хакен и Аппель. Проблема четырех красок родилась в 1852 году, когда Ф.Гютри, раскрашивая карту графств Англии, обнаружил, что трех красок не хватает, а четырех вполне достаточно для того, чтобы никакие два графства одного цвета не имели общей протяженной границы. Четырех красок достаточно для такого раскрашивания вообще любой контурной карты на плоскости - вот теорема о четырех красках. Не будем придираться к ее низкой практической значимости: так ли уж важно сэкономить одну-две краски? Но простота формулировки явно бросала вызов человеческому разуму. Почему-то большинство людей считает, что задачи с простыми условиями имеют столь же простые решения, хотя список до сих пор не решенных проблем свидетельствует как раз об обратном. Уже в следующем, 1853-м, году появилось первое доказательство теоремы о четырех красках - краткое, простое и понятное человеку, но неверное. И потянулась из XIX в XX век цепочка из нескольких дюжин таких же классических по форме, но ошибочных доказательств. До тех пор, пока Хакен и Аппель не опубликовали свое, вызвавшее скандал. Что же они натворили? Ничего, казалось бы, криминального. Они логически свели проблему к раскрашиванию 1482 базовых карт, а затем на компьютере "раскрасили" все эти карты четырьмя красками. К сожалению, раскрашивание потребовало не только четырех красок, но и более 1000 часов машинного времени. Вот этого-то авторам простить никак не могли. Что это за доказательство, которое не в силах проверить вручную ни один человек, ни даже большой коллектив? А вдруг компьютер ошибся? Напрасно Хакен и Аппель оправдывались, что каждый блок их доказательства обязательно проверялся и перепроверялся компьютером разными методами и что при проверке люди напороли бы ошибок куда больше машины. Ценители древнегреческих стандартов оскорбленно отвернулись от их работы как от злостного математического хулиганства и стали ждать появления "настоящего" доказательства. И дождались? Судите сами: доказательство теоремы о четырех красках было упрощено только в 90-х годах, и теперь оно требует раскрашивания "всего лишь" 633 базовых карт, что делается за пару десятков часов на современной персоналке. Разумеется, вручную его никто не проверял, не нашлось таких камикадзе. Но это не помешало "эстетам" неоднократно заявлять, что именно упрощенное доказательство полностью развеяло туман недоверия, окружавший доказательство Хакена и Аппеля. Не удивляйтесь, это они так извиняются за прошлое. Им стыдно сознаться, что туман развеялся сам по себе, когда они свыклись с компьютерами.

Мы забежали в 90-е годы и еще к ним вернемся, но до этого нам следует побывать в 80-х. В 1989 году, через 13 лет после скандального доказательства теоремы о четырех красках, К.Лэм объявил, что ему с сотрудниками удалось доказать знаменитую гипотезу о несуществовании конечной проективной плоскости 10-го порядка, сформулированную Гауссом 200 лет назад. Суть этой гипотезы заключается всего-навсего в том, что таблицу размером 111 на 111 нельзя заполнить нулями и единицами таким образом, чтобы в каждой строке было ровно 11 единиц и в каждом столбце ровно 2 единицы. (Читателю, который возмущенно спросит, кому вообще нужна такая несуществующая таблица, я кратко напомню, что эти чудаки-математики и прочие ученые-фундаментальщики интересуются вовсе не тем, что сегодня можно положить в рот или завтра в кошелек, причем очень даже не напрасно.) Подобно Хакену и Аппелю, Лэм с коллегами сначала логически упростил гипотезу Гаусса насколько было возможно, а затем сломал ее грубой компьютерной силой. Да еще какой силой! Суперкомпьютер Cray-1A за почти 3000 часов чистого машинного времени проанализировал сто триллионов различных вариантов заполнения таблицы, но требуемого условием варианта не обнаружил. Задача решалась супермашиной более двух лет, запускаясь на счет в промежутках между другими задачами. Лэм честно признался, что его доказательство может быть ошибочным с ничтожной вероятностью порядка одной триллионной доли процента. Дело в том, что у Cray-1A случались сбои памяти примерно раз в 1000 часов, и за время анализа гипотезы Гаусса в двух-четырех вариантах из ста триллионов могли появиться ошибки; одна такая ошибка действительно была обнаружена и исправлена. Итак, Лэм не только воспользовался далеко не классическим методом доказательства, но и признал возможность (пусть ничтожную) ошибочности результата. Словом, совсем раскрылся. Но убийственного удара критики не последовало. Напротив, его результат вызвал живой интерес и восторженные отзывы. Хранители древнегреческой простоты доказательств подозрительно молчали. Неужели всего за 13 лет, как злорадно предположил обиженный в свое время Хакен, все они "отошли от дел"? Разумеется, нет. Просто они перевоспитались под давлением новых реалий. Компьютер, бывший в 60-х и 70-х годах уделом избранных, стал в 80-х и 90-х инструментом для всех желающих с ним работать. Даже в такой консервативной области, как чистая математика.

Чтобы не обойти вниманием наши 90-е годы, упомяну еще об одном компьютерном доказательстве, совсем свежем. Для каждого, кто так или иначе связан с компьютерами, что-то слышится родное в словах "булева алгебра". Но для математиков булева алгебра - это аксиоматическая теория. В ее основе лежат три аксиомы, записанные как уравнения в терминах элементов алгебры и операций "и", "или", "не". Первые два уравнения весьма просты, но третье - не очень, причем до недавнего времени эта третья аксиома имела два альтернативных вида. Более старая и длинная формулировка третьей аксиомы булевой алгебры носит имя Хантингтона, более компактную формулировку предложил в 30-х годах Х.Роббинс. Тогда же Роббинс высказал гипотезу, что его аксиоматика полностью эквивалентна старой, но доказать ее не смог. Доказательство было найдено только в 1996 году У.Маккьюном. Это компьютерное доказательство потребовало 8 суток вычислений на рабочей станции Alpha, в процессе которых было выведено из исходных уравнений-аксиом и проанализировано 50000 вспомогательных уравнений с 2600000 членов. Конечно, доказательство Лэма гипотезы Гаусса было более ресурсоемким, но и доказательство Маккьюна тоже никто не возьмется проверить вручную. Впрочем, в наше время никакой психологической потребности в этом уже не осталось.

Если сейчас поставить точку, то у читателя могут возникнуть две ошибочные идеи. Первая: компьютерные доказательства появляются раз в десятилетие, требуют вычислительных суперсредств и касаются только знаменитых проблем "с бородой". Вторая: компьютеры настолько радикально изменили облик математики, что она превратилась чуть ли не в раздел информатики. Такие вредные идеи следует истребить. В наши дни компьютерные доказательства стали явлением обыденным и массовым. Большинство этих доказательств производят (чаще всего о том даже не подозревая) миллионы пользователей систем компьютерной алгебры Mathematica и Maple на платформе Wintel. Действительно, аналитически вычисляя неопределенный интеграл или редуцируя систему полиномиальных уравнений, человек вводит довольно простые исходные выражения и получает от программы довольно простые результаты, совершенно не интересуясь при этом той скрытой огромной работой, которую программа делает за него. Результат доказывается путем вывода, а промежуточные выкладки сразу же уничтожаются программой, да и кому они нужны? Разве это не повседневные маленькие компьютерные доказательства? Как рабочий инструмент, компьютер заменяет исследователю карандаш и бумагу, сохраняя при этом дни и годы его жизни и позволяя достичь ранее недостижимого. Но и только. От этого математика не становится инженерной наукой, а информатика - фундаментальной. У них разные цели и разные пути. Даже если читатель со мной не согласен, я рад, что он дочитал статью и узнал еще об одной грани многогранной применимости компьютеров.

Сергей СЕРЫЙ