Несмотря на всю мою экзистенциальную тревогу о том, что компьютер оставит меня без работы, я должен признать, что инструментом он оказался бесценным. Бывает, что мне нужно объединить целую кучу уравнений в одно уравнение. Если бы я делал это вручную, то почти наверняка где-нибудь ошибся бы. Речь идет о чисто механической процедуре, почти не требующей размышлений: нужно лишь следовать набору правил. Мой лэптоп справляется с этой работой не моргнув глазом, и я доверяю результатам его расчетов гораздо больше, чем плодам своих собственных трудов с карандашом и бумагой. Однако роль компьютера, не сводящаяся к простым манипуляциям с уравнениями, тоже возросла со временем.
Учитывая тесную связь между математикой и алгоритмами, возможно, не должно удивлять, что компьютеры уже почти полвека помогают нам доказывать трудные для понимания математические теоремы. В 1970-х годах компьютер сыграл важную роль в получении решения классической задачи, которую называют «проблемой четырех красок». Эта теорема утверждает следующее: как бы мы ни изменяли границы европейских стран, их карту всегда можно раскрасить, используя не более четырех красок, так, чтобы никакие две страны, имеющие общую границу, не были закрашены одним и тем же цветом. Раскрасить всю карту тремя красками невозможно, но четырех должно хватить.
Доказательство того, что для раскрашивания карты достаточно пяти красок, уже существовало, но никому не удавалось уменьшить это число до четырех. Затем, в 1976 году, два математика – Кеннет Аппель и Вольфганг Хакен – объявили, что нашли способ доказать, что четырех красок достаточно. У их доказательства была одна интересная особенность: они показали, что, хотя разных карт можно нарисовать бесконечное количество, можно показать, что все они могут быть сведены к анализу всего 1936 карт. Но проанализировать такое множество карт вручную было невозможно – или, точнее говоря, невозможно для человека. Аппель и Хакен сумели запрограммировать компьютер на перебор списка карт и проверку их соответствия правилам четырех красок. Неспешному компьютеру 1970-х годов понадобилось более 1000 часов работы, чтобы проанализировать все эти карты.
В задаче, порученной компьютеру, не было ничего творческого. Он занимался тупой, монотонной работой. Но можно ли было доказать, что в программе не было ошибки, которая порождала бы неверные результаты? Вопрос о том, насколько можно доверять работе компьютера, – один из вечных источников тревоги в области разработки искусственного интеллекта. По мере того как мы вступаем в будущее, в котором будут господствовать алгоритмы, обеспечение отсутствия в коде необнаруженных ошибок становится все более трудной задачей.
В 2006 году в журнале Annals of Mathematics было опубликовано полученное при помощи компьютера решение другой классической задачи геометрии – доказательство гипотезы Кеплера. Томас Хейлз, человек, стоявший за этим доказательством, разработал стратегию, позволяющую безоговорочно подтвердить, что шестиугольная стопка, в которую укладывают апельсины в овощной лавке, – самый эффективный вариант упаковки шаров. Ни одна другая конфигурация не занимает меньше места. Подобно Аппелю и Хакену, Хейлз использовал компьютер для анализа конечного, но огромного количества разных вариантов. В 1998 году он объявил о завершении доказательства и представил статью в Annals of Mathematics вместе с кодом программы, которую он использовал в компьютеризованной части работы над доказательством.
Прежде чем статья будет принята к публикации, математики требуют, чтобы все шаги изложенных в ней рассуждений были проверены рецензентами. Они «прогоняют» доказательство в своих умах как программу, чтобы проверить, не выдаст ли оно в каком-нибудь месте ошибку. Однако в этом доказательстве была часть, в которой человеческий разум не мог разобраться из-за своих физических ограничений. Рецензентам приходилось положиться на способности компьютера. Многим это не нравилось. Это было похоже на положение человека, который хочет отправиться из Лондона в Сидней и вынужден впервые в жизни довериться на одном из этапов этого пути самолету. Из-за той роли, которую сыграл в этой работе компьютер, прошло целых восемь лет, прежде чем математики признали доказательство справедливым с 99 %-й вероятностью.
С точки зрения математиков-пуристов, оставшийся 1 % представляет собой непреодолимое препятствие. Представьте себе, что вы доказали, что состоите в родстве с Ньютоном… с точностью до одной недостающей связи в генеалогическом древе. Многие из работающих в этой области отнеслись к применению компьютеров в доказывании теорем с глубоким подозрением. Не то чтобы они опасались, что это может оставить их без работы – в те ранние годы компьютеры могли работать только по приказу математиков, которые их запрограммировали, – но их беспокоило, как можно узнать, не таится ли где-нибудь в глубине программы ошибка. Как можно доверять такому доказательству?