В те дни компьютеры уже начинали потихоньку проникать в мир математики, но тогда они были громадными машинами, которые занимали целые здания, а не стояли спокойно на столе и не умещались в портфеле. Хакена интересовало, можно ли прибегнуть для решения задачи к помощи компьютеров. Оказалось, что такая мысль уже приходила Хеешу в голову, и он даже сделал примерную оценку сложности этой задачи. Из нее следовало, что даже лучший компьютер, к которому он мог бы получить доступ, с ней не справится. В Иллинойсе, однако, был гораздо более мощный компьютер ILLIAC–IV, и Хакен подал заявку на машинное время. Оказалось, однако, что компьютер еще не готов, и ему посоветовали обратиться в Брукхейвенскую лабораторию на Лонг-Айленде, где имелся Cray 6600. Директором компьютерного центра лаборатории был Ёсио Симамото, тоже очарованный задачей о четырех красках. Хееш и Хакен вытянули счастливый билетик — и получили вожделенный доступ к машине.
Компьютер оправдал ожидания, но Хакен начал подозревать, что его можно использовать намного эффективнее. Они генерировали множество сводимых комбинаций и надеялись собрать когда-нибудь из них полный неизбежный набор, но при такой стратегии много времени напрасно растрачивалось на комбинации, которые в конечном итоге оказывались несводимыми. Может быть, лучше поступить наоборот: сделать неизбежность основной целью, а со сводимостью разобраться позже? Конечно, все равно придется брать комбинации с хорошими шансами на сводимость, но сам по себе этот способ казался более перспективным. Однако к этому моменту Cray в Брукхейвене уже был занят более важными вещами. Хуже того, уже несколько специалистов сказали Хакену, что методы, которыми он хочет воспользоваться, вообще невозможно воплотить в компьютерных программах. Он поверил специалистам и прочел лекцию о том, что задача о четырех красках не может быть решена без помощи компьютеров, но теперь, похоже, получается, что с компьютерами ее тоже не решишь. В общем, Хакен решил оставить попытки.
Среди слушателей на лекции присутствовал и опытный программист Кеннет Аппель, который сообщил Хакену, что эксперты, на которых тот ссылается, вероятно, просто хотели избавиться от него, поскольку на создание подобных программ пришлось бы затратить много усилий при непредсказуемом результате. Аппель считал, что математических задач, которые невозможно запрограммировать, не существует. Вопрос только в том, сможет ли программа получить результат за разумное время. Хакен и Аппель объединили усилия. Стратегия, разработанная как модификация все того же метода разрядки, заставляла вносить изменения в программу, а изменения в программе, в свою очередь, заставляли вносить новые изменения в метод. Этот процесс привел к новой концепции «географически подходящих» конфигураций, которые не содержали определенных неподходящих конфигураций, препятствующих сводимости. Шанс на то, что такая конфигурация окажется сводимой, был заметно выше обычного, а определяющее свойство было несложным и легко поддавалось проверке. Аппель и Хакен решили доказать теоретически, а не на компьютере, что существует неустранимое множество географически подходящих конфигураций. К 1974 г. им это удалось.
Это внушало оптимизм, но ученые понимали, что теперь, скорее всего, произойдет: некоторые из географически подходящих конфигураций непременно окажутся несводимыми, так что придется их исключать и заменять на еще более длинный и сложный набор конфигураций. Программа будет «гоняться за собственным хвостом», и успех будет достигнут только в том случае, если этот хвост удастся догнать. Не желая тратить годы на бесплодные поиски, Хакен и Аппель прикинули, сколько времени может занять процесс. Результаты обнадеживали, поэтому работа была продолжена. Теория и расчеты подпитывали и модифицировали друг друга. Временами компьютер, казалось, начинал жить собственной жизнью и проявлять интеллект, «открывая» полезные свойства конфигураций. Затем администрация университета приобрела новый, очень мощный компьютер — более мощный, чем те, что были доступны на тот момент университетским ученым. После многочисленных протестов и споров половина машинного времени была выделена на научные нужды. Вечно меняющийся список неизбежных конфигураций Аппеля и Хакена стабилизировался на уровне примерно 2000 штук. В июне 1976 г. компьютер выполнил последний тест на сводимость, и доказательство было завершено. Благодаря