Доказательство того, что для раскрашивания карты достаточно пяти красок, уже существовало, но никому не удавалось уменьшить это число до четырех. Затем, в 1976 году, два математика – Кеннет Аппель и Вольфганг Хакен – объявили, что нашли способ доказать, что четырех красок достаточно. У их доказательства была одна интересная особенность: они показали, что, хотя разных карт можно нарисовать бесконечное количество, можно показать, что все они могут быть сведены к анализу всего 1936 карт. Но проанализировать такое множество карт вручную было невозможно – или, точнее говоря, невозможно для человека. Аппель и Хакен сумели запрограммировать компьютер на перебор списка карт и проверку их соответствия правилам четырех красок. Неспешному компьютеру 1970-х годов понадобилось более 1000 часов работы, чтобы проанализировать все эти карты.
В задаче, порученной компьютеру, не было ничего творческого. Он занимался тупой, монотонной работой. Но можно ли было доказать, что в программе не было ошибки, которая порождала бы неверные результаты? Вопрос о том, насколько можно доверять работе компьютера, – один из вечных источников тревоги в области разработки искусственного интеллекта. По мере того как мы вступаем в будущее, в котором будут господствовать алгоритмы, обеспечение отсутствия в коде необнаруженных ошибок становится все более трудной задачей.
В 2006 году в журнале Annals of Mathematics было опубликовано полученное при помощи компьютера решение другой классической задачи геометрии – доказательство гипотезы Кеплера. Томас Хейлз, человек, стоявший за этим доказательством, разработал стратегию, позволяющую безоговорочно подтвердить, что шестиугольная стопка, в которую укладывают апельсины в овощной лавке, – самый эффективный вариант упаковки шаров. Ни одна другая конфигурация не занимает меньше места. Подобно Аппелю и Хакену, Хейлз использовал компьютер для анализа конечного, но огромного количества разных вариантов. В 1998 году он объявил о завершении доказательства и представил статью в Annals of Mathematics вместе с кодом программы, которую он использовал в компьютеризованной части работы над доказательством.
Прежде чем статья будет принята к публикации, математики требуют, чтобы все шаги изложенных в ней рассуждений были проверены рецензентами. Они «прогоняют» доказательство в своих умах как программу, чтобы проверить, не выдаст ли оно в каком-нибудь месте ошибку. Однако в этом доказательстве была часть, в которой человеческий разум не мог разобраться из-за своих физических ограничений. Рецензентам приходилось положиться на способности компьютера. Многим это не нравилось. Это было похоже на положение человека, который хочет отправиться из Лондона в Сидней и вынужден впервые в жизни довериться на одном из этапов этого пути самолету. Из-за той роли, которую сыграл в этой работе компьютер, прошло целых восемь лет, прежде чем математики признали доказательство справедливым с 99 %-й вероятностью.
С точки зрения математиков-пуристов, оставшийся 1 % представляет собой непреодолимое препятствие. Представьте себе, что вы доказали, что состоите в родстве с Ньютоном… с точностью до одной недостающей связи в генеалогическом древе. Многие из работающих в этой области отнеслись к применению компьютеров в доказывании теорем с глубоким подозрением. Не то чтобы они опасались, что это может оставить их без работы – в те ранние годы компьютеры могли работать только по приказу математиков, которые их запрограммировали, – но их беспокоило, как можно узнать, не таится ли где-нибудь в глубине программы ошибка. Как можно доверять такому доказательству?
Математики уже обжигались на таких ошибках. В 1992 году оксфордские физики воспользовались эвристическими методами и, исходя из теории струн, высказали некоторые предположения относительно числа алгебраических конструкций, которые могут быть определены в многомерных геометрических пространствах. Математики отнеслись к этому предсказанию с подозрением – откуда физикам знать о столь абстрактных объектах? – и считали, что их сомнения оправдались, когда появилось доказательство, опровергающее эту гипотезу. Оказалось, однако, что в доказательстве содержалась компьютерная составляющая, основанная на программе, в которой была ошибка. Правы были физики, а не математики. Их ввела в заблуждение ошибка в программе. Несколько лет спустя математики сумели доказать (на этот раз без помощи компьютера), что физики были правы.
Подобные истории подпитывают опасения математиков, что компьютеры могут побуждать нас возводить сложные построения на основе программ, имеющих конструктивные дефекты. Но, честно говоря, у человека больше шансов допустить ошибку, чем у компьютера. То, что я сейчас скажу, может показаться ересью, но существуют, вероятно, тысячи доказательств с ненайденными логическими пробелами или ошибками. Мне ли не знать: в паре случаев я обнаруживал логические дыры в своих доказательствах уже после того, как опубликовал их. Эти изъяны поддавались исправлению, но их не заметили ни рецензенты, ни редакторы.
Если речь идет о доказательстве по-настоящему важном, проверка обычно выявляет все нестыковки или ошибки. Именно поэтому премию за решение «задач тысячелетия» присуждают через два года после публикации: считается, что двадцати четырех месяцев должно быть достаточно для выявления любой ошибки. Взять хотя бы первое доказательство Великой теоремы Ферма Эндрю Уайлса. Рецензенты нашли в нем ошибку еще до того, как оно было напечатано. Чудо заключается в том, что Уайлс сумел исправить эту ошибку с помощью своего бывшего ученика Ричарда Тейлора. Но сколько может существовать других ошибочных доказательств, из-за которых мы возводим свои математические здания на ложном фундаменте?
Некоторые новые доказательства настолько сложны, что математики опасаются, что в них могут остаться труднообнаружимые ошибки. Вот, к примеру, классификация конечных простых групп – теорема, близкая к теме моих собственных исследований. Это своего рода периодическая система симметричных атомов, из которых могут быть построены все симметричные объекты. Ее называют «теоремой-монстром», потому что доказательство занимает 10 000 страниц и 100 журнальных статей, в работе над которыми участвовали сотни математиков. В список атомов входят 26 странных и необычных форм, которые называются спорадическими простыми группами. Всегда существовало смутное подозрение, что может существовать и 27-я такая группа, которая, возможно, была пропущена в доказательстве. Способен ли компьютер помочь нам проверить такое сложное доказательство?
Кроме того, если мы заставляем компьютер проверять доказательство и подтверждать обоснованность каждого его шага, не меняем ли мы тем самым шило на мыло? Откуда нам знать, что в самой компьютерной программе, ищущей ошибки, нет своих ошибок? Можно проверить эту программу на наличие ошибок при помощи другого компьютера, но будет ли конец этим проверкам? Эта дилемма всегда преследовала естественные науки и математику. Как можно быть уверенным, что используемые методы ведут к истинному знанию? Любые попытки это доказать неизменно зависят от методологии, достоверность которой мы пытаемся продемонстрировать.
Как первым отметил Юм, наука в значительной степени основывается на процессе, который называется индукцией: выводе общих законов или принципов на основе наблюдения отдельных случаев. Почему эту процедуру можно считать доброкачественным методом получения научной истины?
В целом на основании той же индукции! Мы можем привести множество примеров, в которых принцип индукции порождал, по-видимому, справедливые научные теории. Это позволяет нам заключить (методом индукции), что индукция – действенный подход к занятиям наукой.
По мере появления все новых и новых доказательств, полученных при помощи компьютерных программ, стала ощущаться необходимость в каких-то средствах, позволяющих убедиться, что этим программам можно доверять. В прошлом математические выкладки, созданные людьми, могли проверить люди. Теперь же нужно было создать новые программы для проверки программ, создающих доказательства, так как люди уже не могли проверять их вычисления – они были слишком сложны.
В конце 1980-х годов два французских математика, Жерар Пьер Юэ и Тьерри Кокан, начали работать над проектом под названием «Исчисление конструкций» (Calculus of Constructions, сокращенно CoC). Поскольку во Франции принято давать средствам для научно-технических разработок названия животных, эта система впоследствии стала называться Coq, что означает по-французски «петух». Это название удачно совпало с первыми тремя буквами фамилии одного из создателей системы. Система Coq была создана для проверки доказательств и вскоре стала любимым инструментом всех тех, кого интересует верификация доказательств, созданных компьютерами.
Жорж Гонтье, руководитель исследовательской программы в кембриджском отделении Microsoft Research, решил организовать группу для проверки доказательства теоремы о четырех красках – первого доказательства, для разработки которого потребовался компьютер, – при помощи Coq. К 2000 году эта группа проверила программный код, созданный Аппелем и Хакеном, и подтвердила правильность доказательства (в предположении, что в самой системе Coq нет своих собственных ошибок). После этого при помощи Coq начали проверять «человеческую» часть доказательства – те построения, которые написали сами Аппель и Хакен.
Одна из трудностей проверки доказательства, созданного человеком, состоит в том, что в нем редко бывают изложены все шаги. Люди пишут доказательства не так, как компьютерные программы. Они пишут их для других людей, используя код, который должен работать только на нашем собственном аппаратном обеспечении – в человеческом мозге. Это значит, что, формулируя доказательство, мы часто пропускаем неинтересные или повторяющиеся шаги, зная, что те, кто будет его читать, сумеют восполнить эти пробелы. Но компьютеру необходимы все шаги. В этом разница между сочинением романа, в котором не нужно детально рассказывать о всех банальных действиях героя, и инструктированием новой няньки