Боги из машины Компьютеры снова помогли математикам в доказательстве

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

Одним из основных понятий современной математики является понятие доказательства - последовательности заключений, приводящих к некоторому утверждению (обычно именуемому теоремой) посредством серии умозаключений на основе аксиом и некоторых дополнительных предположений (обычно именуемых условиями теоремы). Знакомство с доказательствами в школе обычно начинается с геометрии. С одной стороны, эта наука дает наиболее наглядные для решения задачи, а геометрические аксиомы приятно формализуются (за что, по большому счету, спасибо Евклиду) в терминах понятных всем объектов - прямых, точек, окружностей.

Но с другой стороны, есть у такого подхода и существенный недостаток. У начавших с геометрии людей может сложиться впечатление, что доказательство должно быть обозримым. То есть таким, чтобы всякий вдумчивый читатель мог бы окинуть его взглядом и, уместив в голове, понять целиком и сразу. Более того, возможность такого осознания для многих (в том числе и профессиональных ученых) становится своего рода синонимом "понятности". Уместил в голове - понятно, не уместил - непонятно.

Осуждать кого-либо за такой подход к математическому доказательству в принципе бессмысленно. Например, в конце XIX века его придерживались почти все математики - доказанным считался только тот факт, в доказательстве которого они (ну или еще какой-то набор специалистов) могли разобраться. Зададимся, однако, вот каким вопросом, который математикам XIX века показался бы, наверное, довольно праздным: как быть, если доказательство нельзя обозреть? Что если одному человеку даже за всю жизнь его просто не прочитать?

Оказывается, такого рода проблемы встречаются сплошь и рядом. Мы поговорим лишь о трех из них.

Задача о четырех красках

В 1852 году некто Франсис Гутри раскрашивал карту Англии. Совершенно случайно он обнаружил, что для работы ему достаточно всего четырех цветов. Франсис был любознательным молодым человеком, поэтому с этим наблюдением он отправился к своему брату, Фредерику, который на тот момент, по счастливому стечению обстоятельств, был студентом у Огастеса де Моргана, великого английского математика, известного, среди прочего, своими законами де Моргана в логике.

Де Морган не смог ни доказать ни опровергнуть утверждение Гутри, но задача его заинтересовала. Впервые в литературу, однако, задача попала в 1879 году благодаря работе Артура Кейли. С этого момента начался нелегкий путь к решению этой задачи. Надо сказать, что они (первые решения, то есть) появились почти сразу - в том же году доказательство опубликовал Альфред Кемпе, а год спустя - Питер Тэт. Оба доказательства считались истинными, пока в 1890 и 1891 годах в обоих рассуждениях не были обнаружены пробелы.

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

Ситуация изменилась в 1976 году. Кеннет Аппель и Вольфганг Хакен предложили необычное решение задачи. Хакен и Аппель свели задачу математическими методами к некоторому конечному набору карт . В разных версиях доказательства это число варьируется от 1400 до 1900. Каждую из этих карт, с точки зрения привычной всем математики, надлежало бы раскрасить от руки, однако Хакен и Аппель применили компьютер.

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

Со временем, однако, буря улеглась, перебор свели к чуть более чем 600 случаев и доказательство было признано верным. В 2004 году оно было проверено при помощи системы Coq, которая специально создана для формализации и проверки математических доказательств (большинство существующих систем совершенно для этого не подходят). Удивительно, кстати, что до сих пор не нашлось шести сотен энтузиастов-математиков, каждый из которых взял бы себе на проверку по одному случаю из доказательства Хакена и Аппеля.

Задача о плотной упаковке

В 1611 году Иоганн Кеплер опубликовал революционную по тем временам работу, посвященную снежинкам, в которой, среди прочего, предлагал решение задачи, подкинутой ему коллегой Томасом Хэрриотом. Хэрриот, который на тот момент служил сэру Уолтеру Рэли, интересовался вопросом, как лучше раскладывать на палубе корабля ядра? "Лучше" в данном случае означало - "чтобы они занимали меньше места". Кеплер предположил, что самой лучшей раскладкой будет размещение шаров так, чтобы их центры образовывали в пространстве гранецентрированную кубическую решетку (на самом деле это не единственный минимальный вариант, но мы остановимся на нем из-за простоты).

В 1831 году Карл Гаусс доказал, что гипотеза Кеплера верна для так называемых регулярных раскладок - то есть, если отвлечься от ядер, то центры шаров образуют в пространстве решетку (о том, что это такое и для чего нужно, "Лента.ру" уже подробно писала). Таким образом, оставалось изучить случай нерешеток.

Существенные сдвиги в этом направлении были сделаны только в XX веке. В 1998 году математик Том Хейлз объявил о найденном им доказательстве гипотезы Кеплера. Ему также удалось свести задачу к конечному перебору, правда во много раз более громоздкому, чем в случае с красками. В рамках своего доказательства Хейлз при помощи компьютера минимизировал функцию от 150-ти переменных на более чем 5 тысячах конфигураций. В каждом случае минимум искался при помощи линейного программирования - всего более 100 тысяч штук.

Во всех случаях минимум оказался больше плотности, даваемой упаковкой Кеплера. В общей сложности, работа велась с 1992 по 1998 годы. Ее результатом стало 250 страниц текста и 3 гигабайта программ и данных. В 1999 году статья была подана в Annals of Mathematics, и комиссия из нескольких десятков специалистов проверяла ее в течение четырех лет. Вердикт ученых был неоднозначный - статья верна на 99 процентов, но все детали компьютерных вычислений им проверить не удалось. В 2006 году Хейлз опубликовал 100-страничную работу, посвященную только некомпьютерной части доказательства.

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

Судоку

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

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

Ответ на этот вопрос нашли ирландские математики (препринт). Им удалось доказать, что всего подсказок должно быть как минимум 17. Примечательно, что однозначно разрешимые головоломки с 17 подсказками и головоломки с несколькими решениями и 16 подсказками раньше уже были известны.

В работе ученые тоже сначала использовали математику - они описали все возможные решенные судоку и пришли к выводу, что их все не надо рассматривать. Дело в том, что некоторые таблицы получаются друг из друга набором простых операций (например, поворота вокруг центра квадрата на 90 градусов). Благодаря этому им пришлось рассмотреть не 6 670 903 752 021 072 936 960 вариантов, а всего 5 472 730 538.

Для каждого такого варианта они описали множества - наборы цифр в заполненной таблице, которые могут быть заменены на другие. Эти множества были названы плохими, поскольку из-за них и возникает неоднозначность. Это позволило значительно ускорить проверку каждого варианта на предмет, можно ли его получить, стартуя с 16-ти подсказок.

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

Вместо заключения

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