В общем, Хакен решил оставить попытки.
Среди слушателей на лекции присутствовал и опытный программист Кеннет Аппель, который сообщил Хакену, что эксперты, на которых тот ссылается, вероятно, просто хотели избавиться от него, поскольку на создание подобных программ пришлось бы затратить много усилий при непредсказуемом результате. Аппель считал, что математических задач, которые невозможно запрограммировать, не существует. Вопрос только в том, сможет ли программа получить результат за разумное время. Хакен и Аппель объединили усилия. Стратегия, разработанная как модификация все того же метода разрядки, заставляла вносить изменения в программу, а изменения в программе, в свою очередь, заставляли вносить новые изменения в метод. Этот процесс привел к новой концепции «географически подходящих» конфигураций, которые не содержали определенных неподходящих конфигураций, препятствующих сводимости. Шанс на то, что такая конфигурация окажется сводимой, был заметно выше обычного, а определяющее свойство было несложным и легко поддавалось проверке. Аппель и Хакен решили доказать теоретически, а не на компьютере, что существует неустранимое множество географически подходящих конфигураций. К 1974 г. им это удалось.
Это внушало оптимизм, но ученые понимали, что теперь, скорее всего, произойдет: некоторые из географически подходящих конфигураций непременно окажутся несводимыми, так что придется их исключать и заменять на еще более длинный и сложный набор конфигураций. Программа будет «гоняться за собственным хвостом», и успех будет достигнут только в том случае, если этот хвост удастся догнать. Не желая тратить годы на бесплодные поиски, Хакен и Аппель прикинули, сколько времени может занять процесс. Результаты обнадеживали, поэтому работа была продолжена. Теория и расчеты подпитывали и модифицировали друг друга. Временами компьютер, казалось, начинал жить собственной жизнью и проявлять интеллект, «открывая» полезные свойства конфигураций. Затем администрация университета приобрела новый, очень мощный компьютер — более мощный, чем те, что были доступны на тот момент университетским ученым. После многочисленных протестов и споров половина машинного времени была выделена на научные нужды. Вечно меняющийся список неизбежных конфигураций Аппеля и Хакена стабилизировался на уровне примерно 2000 штук. В июне 1976 г. компьютер выполнил последний тест на сводимость, и доказательство было завершено. Благодаря The Times эта история попала в средства массовой информации и стремительно разлетелась по всему миру.
Аппелю и Хакену еще нужно было убедиться, что в доказательстве нет глупых ошибок и упущений, а несколько групп ученых уже устремились по их следам. К июлю, уверившись в действенности своего метода, Аппель и Хакен официально объявили математическому сообществу, что им удалось доказать теорему о четырех красках. Они выпустили препринт — предварительный вариант статьи, который печатается до выхода в свет основной публикации. В то время на публикацию серьезной математической статьи обычно уходило от одного до двух лет. Чтобы не сдерживать прогресс, математикам приходилось искать более быстрые способы познакомить профессиональное сообщество с важными результатами, и препринты были одним из них. В наши дни препринты, как правило, публикуются в Интернете. Полная официальная публикация требует рецензирования, и препринты помогают в ее подготовке — ведь кто угодно может читать их, искать ошибки и сообщать о них авторам, а также предлагать улучшения. Именно поэтому опубликованная версия статьи часто сильно отличается от препринтной.
Окончательное доказательство потребовало около 1000 часов компьютерного времени и содержало 487 правил разрядки. Результаты были опубликованы в двух статьях с 450-страничным приложением, в котором показаны все 1482 конфигурации. На тот момент это был верх совершенства. |