Компьютер подтвердил: пятый цвет не нужен

Доказательство теоремы о четырех красках, сформулированной Фрэнсисом Гатри в далеком 1852 году, было получено математиками из США Кеннетом Эппелем (Kenneth Appel) и Вольфгангом Хакеном (Wolfgang Haken) еще в 1976 году. Согласно этой теореме, четырех цветов достаточно для раскраски географической карты таким образом, чтобы две «страны», обозначенные одним и тем же цветом, никогда не граничили бы друг с другом. Тем не менее, ключевой элемент их работы, заключавшийся в проверке многих тысяч карт, удалось выполнить лишь при помощи компьютера. До сих пор у математиков имелись подозрения, что положительный результат мог явиться следствием программных ошибок. Теперь же, сообщает New Scientist, Джорджу Гонтье (Georges Gonthier) из исследовательской лаборатории Microsoft в Кембридже (Великобритания) и Бенджамину Вернеру (Benjamin Werner) из французского INRIA удалось подтвердить абсолютную строгость доказательства тридцатилетней давности.

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

«Это – важная веха, - заявил Рэнди Поллак (Randy Pollack) из Эдинбургского университета в Шотландии, автор одной из первых программ проверки логики, написанной на Coq. – В первую очередь из-за того, что в данном случае речь идет о столь широко известной теореме, а также из-за того, что в 1976 году это доказательство наделало немало шума».

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

Джордж Гонтье указывает на то, что знай математики о том, что они смогут убедительно продемонстрировать логичность своих выкладок, они во все большем числе станут использовать компьютеры. Это, в свою очередь, может со временем изменить мышление многих из них. «Я уже обнаружил, что в определенных обстоятельствах поступаю совершенно по-иному только из-за того, что использую компьютер», - сказал он.

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

«Данное открытие окажет значительное воздействие на будущее компьютеров, - заявил Эндрю Герберт (Andrew Herbert), управляющий директор Microsoft Research Cambridge. – Достигнутые нами успехи в области разработки контролирующего самого себя программного обеспечения, в принципе позволяют использовать их в средствах разработки ПО, что сделает программные продукты более надежными и повысит уровень доверия пользователей к ним».