, при котором приходится описывать весь день в мельчайших подробностях, в том числе о времени дневного сна, хождении в туалет и всех до последнего пунктах меню ребенка.
Подтверждение правильности человеческой части доказательства заняло у компьютера пять лет. У этого процесса были и интересные побочные результаты: исследователи открыли новые и довольно неожиданные математические жемчужины, которых не заметили авторы исходного доказательства.
Почему же мы должны доверять программе Coq больше, чем исходному компьютерному доказательству? Ответ на этот вопрос, что интересно, связан с индукцией. По мере того как система Coq подтверждает все больше доказательств, в правильности которых мы уверены, мы все больше убеждаемся в том, что в ней самой нет ошибок. По сути дела, тут работает тот же принцип, который мы используем для проверки фундаментальных математических аксиом. Тот факт, что, какие бы числа А и В мы ни взяли, результаты сложения А + + В и сложения В + А получаются одинаковыми, заставляет нас признать справедливость аксиомы, утверждающей, что А + В = В + А. Используя одну и ту же программу для проверки всех остальных, мы можем доверять ее заключениям больше, чем если бы мы работали с какой бы то ни было специализированной программой, специально созданной для проверки данного конкретного доказательства.
Когда группа Гонтье закончила проверку теоремы о четырех красках, он поставил перед ней новую задачу – теорему о нечетном порядке[70]. Это одна из самых важных теорем, направляющих исследования симметрии. Ее доказательство привело к созданию классификации конечных простых групп, перечня основополагающих элементов, из которых можно построить все симметричные объекты. Один из самых простых элементов в этой периодической системе – правильные двумерные многоугольники с простым числом сторон, такие как треугольник или пятиугольник. Но существуют и гораздо более сложные и экзотические примеры симметрий, от 60 вращательных симметрий икосаэдра до симметрий странной снежинки в 196 883-мерном пространстве: число ее симметрий больше количества атомов, входящих в состав Земли.
Теорема о нечетном порядке утверждает, что для построения любого симметричного объекта с нечетным числом симметрий не требуются никакие экзотические симметрии. Он может быть составлен из простых элементов многоугольника, количество сторон которого равно простому числу. Эта теорема важна, потому что она исключает из рассмотрения половину возможных объектов. С этого момента мы можем предполагать, что объекты, которые мы пытаемся идентифицировать, обладают четным числом симметрий.
Доказательство этой теоремы было довольно устрашающим. В нем было 255 страниц, и его публикация заняла целый выпуск журнала Pacific Journal of Math. До его появления доказательства по большей части занимали не более нескольких страниц, и в них можно было разобраться за день. Это же доказательство было таким длинным и сложным, что понять его было непростой задачей для любого математика. Учитывая его размеры, нельзя было не заподозрить, что где-то среди его многочисленных страниц может таиться какая-нибудь малозаметная ошибка.
Поэтому проверка этого доказательства при помощи Coq не только продемонстрировала бы мастерство этой системы: она укрепила бы нашу уверенность в справедливости доказательства одной из самых сложных теорем в математике. Это была достойная цель. Но преобразование доказательства, созданного человеком, в проверяемый код делало эту задачу еще более грандиозной. Гонтье предстояла нелегкая работа.
Он смущенно вспоминал:
Когда мы собрались и я впервые обнародовал свой великий план, группа сначала решила, что у меня мания величия. Но настоящей целью проекта было разобраться с доказательством, которое на момент начала этой работы явно считалось недосягаемым, понять, как создавать все эти теории, как добиваться их соответствия друг другу и как убеждаться в правильности всего этого.
После совещания один из программистов просмотрел доказательство. О своих впечатлениях он написал Гонтье по электронной почте: «Число строк – 170 000. Число определений – 15 000. Число теорем – 4300. Развлечений – масса!» Группа из кембриджского отделения Microsoft Research потратила на работу над этим доказательством шесть лет. Гонтье рассказывал о том восторге, который он ощущал по мере приближения проекта к завершению. Наконец, после множества бессонных ночей, он мог успокоиться.
«Математика – одна из последних великих романтических дисциплин, – сказал он, – в которой одному гению, по сути дела, приходится держать в голове и понимать сразу всё». Но аппаратное обеспечение человека подходит к пределу своих возможностей. Гонтье надеется, что его работа положит начало эпохе большего доверия и устойчивого сотрудничества между человеком и машиной.
Среди молодых математиков сейчас растет ощущение, что многие области математического мира становятся настолько дремучими и сложными, что все три года аспирантуры можно потратить только на то, чтобы понять ту задачу, которую поставил тебе научный руководитель. Можно работать долгие годы, осваивая эту территорию и отмечая на карте свои открытия, а затем обнаружить, что ни у кого другого нет ни сил, ни времени пройти тем же путем, чтобы понять или проверить их.
Повторение чужой работы – дело не слишком благодарное. Однако именно на нем основывается рецензирование статей в научных журналах. Карьерный рост и получение постоянной научной работы зависят от признания, которое дает публикация работ в журналах уровня Annals of Mathematics[71] или Les Publications mathématiques de l’IHES[72]. Поэтому роль систем, подобных Coq, в проверке доказательств теорем, претендующих на публикацию в таких журналах, может становиться все более значительной.
Некоторым из математиков кажется, что мы подходим к концу эпохи. Та математика, в которой способен ориентироваться человеческий разум, неизбежно должна иметь пределы. Взять хотя бы классификацию конечных простых групп, составных элементов симметрии. Тот факт, что мы, люди, сумели при помощи собственного разума, карандаша и бумаги построить симметричный объект, который может быть построен только в 196 833-мерном пространстве, поразителен. Те математики, которые по-настоящему уверенно разбираются в симметриях группы-монстра, стареют. Подобно средневековым каменщикам, они владеют мастерством, которое будет утрачено с их смертью. У тех, кто идет за ними, нет особого стимула повторять эти готические шедевры, если только они не открывают дорогу к новым чудесам.
Сотни страниц журнальных статей, написанные в течение трех столетий, чтобы доказать, что уравнения Ферма не имеют решений, свидетельствуют о том, какую долгую игру способен вести человеческий разум. И все же при работе над доказательством гипотезы всегда возникает смутное ощущение, что сложность доказательства может превосходить пределы физических возможностей человеческого мозга. Мы способны на поразительные свершения, но математика бесконечна, а мы конечны: мы можем математически доказать, что математика больше, чем можем быть мы.
Сейчас я работаю над гипотезой, которая не отпускает меня уже пятнадцать лет. Каждый раз, когда я пытаюсь собрать воедино идеи, появившиеся у меня относительно разных частей моей задачи, мой мозг выдает «сообщение о переполнении». Решение завораживающе близко, но я никак не могу собрать все его части в единое целое. Такое со мной уже случалось, и я знаю, что иногда, чтобы поймать решение задачи, этого дикого зверя, в сети, которые расставляет на него мой разум, нужно суметь взглянуть на него с новой стороны. Когда целые поколения математиков безуспешно бьются над доказательством, например, гипотезы Римана, величайшей из нерешенных задач в области простых чисел, кто-нибудь неизбежно должен задуматься, не лежит ли это доказательство за пределами возможностей человеческого мозга – при всей простоте формулировки этой гипотезы.
Г.Г. Харди, потративший много лет на бесплодную борьбу с гипотезой Римана, язвительно заметил: «Любой дурак может задать такой вопрос о простых числах, на который не сумеет ответить и мудрейший из мудрецов». Австрийский логик Курт Гёдель доказал, что в математике существуют истинные утверждения, для которых не может быть доказательств. Это открытие было в некотором смысле ужасным. Нужно ли нам ввести новые аксиомы, чтобы уловить эти недоказуемые истины? В 1951 году Гёдель предупреждал, что современная математика, вероятно, будет все больше и больше удаляться от нашего понимания:
Перед нами возникает бесконечная последовательность аксиом, которая может быть продолжена все дальше и дальше, и конца ей не видно. Правда, высшие уровни этой иерархии в современной математике практически никогда не используются… вполне вероятно, что это свойство нынешней математики может быть как-то связано с ее неспособностью доказать некоторые фундаментальные теоремы – такие, например, как гипотеза Римана.
Учитывая, что мы, возможно, приближаемся к полному исчерпанию человеческих возможностей, некоторые математики начинают признавать, что для дальнейшего продвижения вперед нам понадобятся машины. Чтобы подняться на вершину Эвереста, нам не нужно почти ничего, кроме баллона с кислородом, но мы никогда не смогли бы добраться до Луны без сотрудничества человека с машиной.
Один из тех, кто считает, что дни одинокого математика, работающего с карандашом и бумагой, сочтены, – Дорон Зайльбергер, израильский математик, который пишет статьи в сотрудничестве с компьютером с 1980-х годов и настаивает, чтобы его машина, Шалош Б. Эхад, признавалась соавтором всех статей, в работе над которыми он используют компьютер. «Шалош Б. Эхад» – это прочитанное на иврите название 3В1, марка машины фирмы AT