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

Как первым отметил Юм, наука в значительной степени основывается на процессе, который называется индукцией: выводе общих законов или принципов на основе наблюдения отдельных случаев. Почему эту процедуру можно считать доброкачественным методом получения научной истины?

В целом на основании той же индукции! Мы можем привести множество примеров, в которых принцип индукции порождал, по-видимому, справедливые научные теории. Это позволяет нам заключить (методом индукции), что индукция – действенный подход к занятиям наукой.

Coq – проверщик доказательств

По мере появления все новых и новых доказательств, полученных при помощи компьютерных программ, стала ощущаться необходимость в каких-то средствах, позволяющих убедиться, что этим программам можно доверять. В прошлом математические выкладки, созданные людьми, могли проверить люди. Теперь же нужно было создать новые программы для проверки программ, создающих доказательства, так как люди уже не могли проверять их вычисления – они были слишком сложны.

В конце 1980-х годов два французских математика, Жерар Пьер Юэ и Тьерри Кокан, начали работать над проектом под названием «Исчисление конструкций» (Calculus of Constructions, сокращенно CoC). Поскольку во Франции принято давать средствам для научно-технических разработок названия животных, эта система впоследствии стала называться Coq, что означает по-французски «петух». Это название удачно совпало с первыми тремя буквами фамилии одного из создателей системы. Система Coq была создана для проверки доказательств и вскоре стала любимым инструментом всех тех, кого интересует верификация доказательств, созданных компьютерами.

Жорж Гонтье, руководитель исследовательской программы в кембриджском отделении Microsoft Research, решил организовать группу для проверки доказательства теоремы о четырех красках – первого доказательства, для разработки которого потребовался компьютер, – при помощи Coq. К 2000 году эта группа проверила программный код, созданный Аппелем и Хакеном, и подтвердила правильность доказательства (в предположении, что в самой системе Coq нет своих собственных ошибок). После этого при помощи Coq начали проверять «человеческую» часть доказательства – те построения, которые написали сами Аппель и Хакен.

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

Подтверждение правильности человеческой части доказательства заняло у компьютера пять лет. У этого процесса были и интересные побочные результаты: исследователи открыли новые и довольно неожиданные математические жемчужины, которых не заметили авторы исходного доказательства.

Почему же мы должны доверять программе Coq больше, чем исходному компьютерному доказательству? Ответ на этот вопрос, что интересно, связан с индукцией. По мере того как система Coq подтверждает все больше доказательств, в правильности которых мы уверены, мы все больше убеждаемся в том, что в ней самой нет ошибок. По сути дела, тут работает тот же принцип, который мы используем для проверки фундаментальных математических аксиом. Тот факт, что, какие бы числа А и В мы ни взяли, результаты сложения А + + В и сложения В + А получаются одинаковыми, заставляет нас признать справедливость аксиомы, утверждающей, что А + В = В + А. Используя одну и ту же программу для проверки всех остальных, мы можем доверять ее заключениям больше, чем если бы мы работали с какой бы то ни было специализированной программой, специально созданной для проверки данного конкретного доказательства.

Когда группа Гонтье закончила проверку теоремы о четырех красках, он поставил перед ней новую задачу – теорему о нечетном порядке[70]. Это одна из самых важных теорем, направляющих исследования симметрии. Ее доказательство привело к созданию классификации конечных простых групп, перечня основополагающих элементов, из которых можно построить все симметричные объекты. Один из самых простых элементов в этой периодической системе – правильные двумерные многоугольники с простым числом сторон, такие как треугольник или пятиугольник. Но существуют и гораздо более сложные и экзотические примеры симметрий, от 60 вращательных симметрий икосаэдра до симметрий странной снежинки в 196 883-мерном пространстве: число ее симметрий больше количества атомов, входящих в состав Земли.

Теорема о нечетном порядке утверждает, что для построения любого симметричного объекта с нечетным числом симметрий не требуются никакие экзотические симметрии. Он может быть составлен из простых элементов многоугольника, количество сторон которого равно простому числу. Эта теорема важна, потому что она исключает из рассмотрения половину возможных объектов. С этого момента мы можем предполагать, что объекты, которые мы пытаемся идентифицировать, обладают четным числом симметрий.

Доказательство этой теоремы было довольно устрашающим. В нем было 255 страниц, и его публикация заняла целый выпуск журнала Pacific Journal of Math. До его появления доказательства по большей части занимали не более нескольких страниц, и в них можно было разобраться за день. Это же доказательство было таким длинным и сложным, что понять его было непростой задачей для любого математика. Учитывая его размеры, нельзя было не заподозрить, что где-то среди его многочисленных страниц может таиться какая-нибудь малозаметная ошибка.

Поэтому проверка этого доказательства при помощи Coq не только продемонстрировала бы мастерство этой системы: она укрепила бы нашу уверенность в справедливости доказательства одной из самых сложных теорем в математике. Это была достойная цель. Но преобразование доказательства, созданного человеком, в проверяемый код делало эту задачу еще более грандиозной. Гонтье предстояла нелегкая работа.