Какую часть математических доказательств можно поручить компьютеру? Какие существуют виды интерактивных систем поиска математических доказательств? В чем заключается теорема о четырех красках? И как она была доказана? Математик Лев Беклемишев о теории множеств, интерактивных системах и проблеме о четырех красок.

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


Необходимо вспомнить достижения логики начала ХХ века, которые говорят о том, что, с одной стороны, математические доказательства могут быть полностью сведены к преобразованиям конечных последовательностей символов в рамках некоторых формальных систем, таких как теория множеств. То есть известен конечный набор аксиом и правил, по которым можно вывести в принципе любое доказуемое математическое утверждение. Однако, с другой стороны, не существует алгоритма, который позволяет по данному высказыванию в какой-то конкретной формальной системе узнать, доказуемо оно или нет. Единственное, что может делать компьютер, — это постепенно в результате процесса вычисления порождать всё новые высказывания, выводимые в данной формальной системе, и этот процесс потенциально никогда не заканчивается. Так как мы не можем заранее знать, встретится или нет в этом перечислении интересующий нас результат, мы не можем рассчитывать и на построение его формального доказательства за конечное время.

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

Приблизительно лет пятнадцать-двадцать назад развитие компьютерных технологий достигло такого уровня, когда стало возможно всерьез надеяться на создание систем, которые действительно могли бы помочь работе математика при построении и проверке математических доказательств, то есть фактически взять на себя часть его интеллектуальной работы. На данный момент эта область очень быстро развивается, и существует больше десятка различных систем, предназначенных для автоматического и полуавтоматического, то есть интерактивного, доказательства теорем. Для этих систем появилось специфическое название «прувер».


Системы делятся на два класса: автоматические, которые ищут доказательства совершенно независимо от человека, и интерактивные, которые взаимодействуют с человеком; он помогает компьютеру находить эти доказательства. И именно такие интерактивные системы наиболее перспективны для формализации реальных математических доказательств. И даже среди таких интерактивных систем существует довольно большая конкуренция. В настоящее время наиболее известны несколько: одна из них — это система Coq, разрабатываемая во Франции, есть конкурирующие с ней системы HOL, NuPRL и другие.

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


Что такое теорема о четырех красках? Она долгое время была недоказанной математической гипотезой и состояла в том, что каждую карту на плоскости можно раскрасить правильным образом в четыре цвета. "Правильным образом" — это означает, что разные страны на этой карте, если они имеют общий участок границы, должны быть покрашены в разные цвета. Если исключить некоторые патологические ситуации, то хорошие карты на плоскости в соответствии с этой теоремой о четырех красках всегда можно раскрасить в четыре цвета.

История этой задачи довольно интересная. Высказал эту гипотезу впервые один любитель математики по фамилии Гутри в ХIХ веке. Через 10 лет было предложено два доказательства этого результата, в которых быстро нашли ошибки. И с тех пор эта задача приобрела статус очень известной математической гипотезы, которая оставалась недоказанной в течение более ста лет.

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

Само сведение к тысяче случаев было далеко не тривиальным и в общем занимало несколько сотен страниц, то есть это был очень сложный математический результат, сопровождаемый еще сложным перебором. И при уровне развития компьютерной техники в те времена надеяться на то, что все в этом переборе правильно, было нельзя. Не все признавали эту теорему доказанной, и оставалось только верить компьютеру, что он не ошибся.

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

И по-прежнему, поскольку компьютер участвовал в этом процессе, у математиков не было доверия к полученному решению. После этого за дело взялись специалисты по формальной математике, потому что было понятно, что здесь как раз тот случай, когда построение полностью формализованного и проверенного (как говорят в таких случаях, «верифицированного») доказательства теоремы может спасти положение и убедить всех в ее корректности. А такую верификацию можно также было сделать только с помощью компьютера.

Эта работа заняла несколько лет, группа французских ученых под руководством Жоржа Гонтье завершила ее в 2004 году, и с помощью одной из таких систем интерактивного поиска вывода, системы Coq, они на этот раз формально доказали гипотезу о четырех красках. При этом им пришлось верифицировать как содержательную часть доказательства, сведение к перебору, так и формально доказать корректность алгоритма той программы, которая осуществляла перебор. В этом было принципиальное отличие их работы от предыдущих доказательств этой теоремы: компьютерное вычисление было снабжено компьютерным же доказательством его корректности. Конечно, это был успех, потому что формальные верифицированные математические доказательства имеют гораздо большую надежность, чем любое сколько-нибудь объемное доказательство, полученное человеком. Таким образом, теорему о четырех красках, при всей ее громоздкости, можно считать на данный момент одним из наиболее тщательно проверенных и надежно установленных математических результатов.


Этот случай, конечно, стал очень известен, о нем публиковали в газете New York Times, но насколько надежными в принципе могут быть компьютерные доказательства? И вообще, где гарантия того, что какие-то логические построения и выводы, которые получает компьютер, более надежны, чем обычные компьютерные программы, в которых, как известно, часто встречаются ошибки? Всякий, кто пользовался персональным компьютером, наверняка имел возможность в этом убедиться на собственном опыте.

Для систем компьютерного доказательства, конечно, критично иметь высокую надежность. Абсолютной надежности тем не менее не гарантирует ни один прувер, а относительную, но очень хорошую надежность гарантирует архитектура этих систем. Дело в том, что в идеале такая компьютерная система должна соответствовать так называемому принципу де Брейна, названному в честь голландского специалиста по информатике. Этот принцип состоит в следующем: система состоит из двух частей, из маленького и просто описываемого ядра, которое называется логическим ядром и которое представляет собой примерно то же самое, что и формальная система. Логическое ядро задается набором правил, по которым генерируются формальные доказательства. Это логическое ядро может быть снабжено верификатором, то есть модулем, который проверяет, соответствует ли данный формальный текст этим логическим правилам. Поскольку логических правил мало и ядро маленькое, то такой верификатор не занимает много места и сравнительно прост. Более того, каждый человек может при желании написать свой собственный верификатор, который проверит, верно построенное формальное доказательство или нет.

А помимо этого логического ядра имеется большой модуль, который не обязан быть таким уж простым, а может быть сколь угодно сложным. Это система, которая облегчает взаимодействие человека с ядром или с компьютером. И надежность получаемых доказательств не зависит от того, насколько большая или надежная эта дополнительная часть. В худшем случае, если в дополнительной части не все в порядке, у пользователя просто не получится построить часть доказательств, но все построенные будут корректными с точки зрения ядра.

К сожалению, принцип де Брейна в реально существующих системах выдерживается не всегда, не все пруверы могут явно сгенерировать полностью формальный текст доказательства. Встречаются непрозрачные тактики поиска вывода, но тем не менее, по большому счету, эти системы дают лучшую гарантию надежности, чем любые другие методы, в том числе традиционное «ручное» доказательство теорем.


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

Лев Беклемишев — доктор физико-математических наук, член-корреспондент РАН, главный научный сотрудник Математического института им. В.А. Стеклова РАН, профессор факультета математика ВШЭ.

ПостНаука