Изменить размер шрифта - +
Что же касается проблемы четырех красок, то с ней дело обстояло иначе: она никем не была и не будет полностью проверена.

За двадцать лет, прошедших с тех пор, как Хакен и Аппель сообщили о доказательстве теоремы о четырех красках, компьютеры неоднократно использовались для решения других, менее известных, но столь же важных проблем. В математике — области, не ведавшей ранее вмешательства столь современной технологии, как компьютеры, — все больше и больше специалистов неохотно осваивали использование кремниевой логики и разделяли мнение Вольфганга Хакена: «Всякий, в любом месте доказательства, может полностью вникнуть в детали и проверить их. То, что компьютер может за несколько часов «просмотреть» столько деталей, сколько человек не сможет просмотреть за всю свою жизнь, не меняет в принципе представление о математическом доказательстве. Меняется не теория, а практика математического доказательства».

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

Специалист в области «computer science» Эдвард Френкин даже заявил, что когда-нибудь компьютер найдет решение какой-нибудь важной проблемы без помощи математиков. Десять лет назад Френкин учредил премию Лейбница размером в 100000 долларов. Премия будет присуждена первой компьютерной программе, способной сформулировать и доказать теорему, которая окажет «глубокое влияние на развитие математики». Будет ли когда-нибудь присуждена премия Лейбница — вопрос спорный, но одно можно сказать со всей определенностью: компьютерной программе всегда будет недоставать прозрачности традиционных доказательств, и в сравнении с ними она будет проигрывать, уступая им в глубине. Математическое доказательство должно не только давать ответ на поставленный вопрос, но и способствовать пониманию, почему ответ именно таков, каков он есть, и в чем именно состоит его суть. Задавая вопрос на входе в черный ящик и получая ответ на выходе из него, мы увеличиваем знание, но не понимание. Из представленного Уайлсом доказательства Великой теоремы Ферма мы узнали, что уравнение Ферма не допускает решений в целых числах потому, что любое такое решение привело бы к противоречию с гипотезой Таниямы-Шимуры. Уайлс не только ответил на вызов Ферма, но и обосновал свой ответ, указав, что он должен быть именно таким, а не другим, чтобы не нарушить фундаментальное соответствие между эллиптическими кривыми и модулярными формами.

Математик Рональд Грэхем описывает недостаточную глубину компьютерных доказательств на примере одной из великих не доказанных по сей день гипотез — гипотезы Римана: «Я был бы весьма и весьма разочарован, если бы можно было подключиться к компьютеру, спросить у него, верна ли гипотеза Римана, и получить в ответ: "Да, верна, но Вы не сможете понять доказательство"».

Быстрый переход