home | login | register | DMCA | contacts | help |      
mobile | donate | ВЕСЕЛКА

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
А Б В Г Д Е Ж З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Э Ю Я


my bookshelf | genres | recommend | rating of books | rating of authors | reviews | new | форум | collections | читалки | авторам | add
fantasy
space fantasy
fantasy is horrors
heroic
prose
  military
  child
  russian
detective
  action
  child
  ironical
  historical
  political
western
adventure
adventure (child)
child's stories
love
religion
antique
Scientific literature
biography
business
home pets
animals
art
history
computers
linguistics
mathematics
religion
home_garden
sport
technique
publicism
philosophy
chemistry
close

реклама - advertisement






 Рис. 28.

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

Хакен и Аппель изучили работу Генриха Хееша, утверждавшего, что из некоторого конечного числа карт, содержащих конечное число областей, можно построить бесконечное множество разнообразнейших карт. Изучение карт, составленных из таких строительных блоков, позволяет составить представление о том, как следует искать подходы к решению общей проблемы четырех красок. Основные карты можно рассматривать как эквиваленты электрона, протона и нейтрона — фундаментальных «кирпичиков», из которых построено все остальное. Хакену и Аппелю удалось свести проблему четырех красок «всего лишь» к 1482 конфигурациям, служащим теми строительными блоками, из которых можно составить любую карту. Если бы Хакен и Аппель смогли доказать, что каждый из этих строительных блоков может быть раскрашен четырьмя красками, то из этого следовало бы, что все карты также могут быть раскрашены в четыре краски.

Разумеется, проверка всех 1482 карт и перебор различных комбинаций раскраски каждой из них — задача необычайно громоздкая и трудоемкая, заведомо выходящая за рамки возможностей любой группы математиков. Даже при использовании компьютера перебор возможных вариантов мог бы затянуться на столетие. Но Хакен и Аппель не пали духом и принялись разыскивать удачные ходы и стратегии, использование которых позволило бы ускорить проверку карт и вариантов их раскрашивания. В 1975 году, через пять лет после того как они приступили к работе над проблемой четырех красок, Хакен и Аппель стали свидетелями, что компьютер не только выполняет вычисления, но и делает нечто большее, а именно привносит в работу новые идеи. Хакен и Аппель вспоминают поворотный пункт в их исследовании: «Когда мы дошли до этого пункта, программа начала удивлять нас. Первое время мы проверяли от руки все ее вычисления и могли всегда предсказать, как она будет работать в любой ситуации; но теперь она неожиданно повела себя, как шахматная машина. Программа стала выдавать составные стратегии, используя всевозможные трюки, которым она «научилась», и часто предлагаемые программой подходы оказывались более умными, чем те, которые могли предложить мы сами. Так программа стала учить нас, как действовать, чего мы от нее никак не ожидали. В каком-то смысле программа превзошла нас, ее создателей, не только в механической, но и в «интеллектуальной» части работы».

В июне 1976 года, затратив 1200 часов машинного времени, Хакен и Аппель заявили во всеуслышание, что им удалось проанализировать все 1482 карты и для раскрашивания ни одной из них не требуется более четырех красок. Проблема четырех красок Гатри была наконец решена. Следует особенно подчеркнуть, что решение проблемы четырех красок стало первым математическим доказательством, в котором роль компьютера не сводилась к ускорению вычислений, — компьютер привнес в решение проблемы нечто гораздо большее: его роль была столь значительной, что без компьютера получить доказательство было бы невозможно. Решение проблемы четырех красок с помощью компьютера было выдающимся достижением, но в то же время оно вызвало у математического сообщества чувство тревоги, так как проверка доказательства в традиционном смысле не представлялась возможной.

Прежде, чем опубликовать решение Хакена и Аппеля на страницах «Illinois Journal of Mathematics», редакторам было необходимо подвергнуть его тщательному рецензированию в каком-то не известном ранее смысле. Традиционное рецензирование было невозможно, поэтому было решено ввести программу Хакена и Аппеля в независимый компьютер с тем, чтобы убедиться, что результат останется тем же.

Такое нестандартное рецензирование привело в ярость некоторых математиков, утверждавших, будто компьютерная поверка неадекватна, так как не дает гарантии от внезапного отказа в недрах компьютера, который может стать причиной сбоя в логике. X.П.Ф. Суиннертон-Дайер высказал следующее замечание по поводу компьютерных доказательств: «Когда теорема доказана с помощью компьютера, невозможно изложить доказательство в соответствии с традиционным критерием — так, чтобы достаточно терпеливый читатель смог шаг за шагом повторить доказательство и убедиться в том, что оно верно. Даже если бы кто-нибудь взял на себя труд распечатать все программы и все данные, использованные в доказательстве, нельзя быть уверенным в абсолютно правильной работе компьютера. Кроме того, у любого современного компьютера по каким-то неясным причинам могут быть слабые места как в программном обеспечении, так и в электронном оборудовании, которые могут приводить к сбоям так редко, что остаются необнаруженными на протяжении нескольких лет, и поэтому в работе каждого компьютера могут быть незамеченные ошибки».

До какой-то степени поведение математического сообщества, предпочитавшего избегать компьютеров вместо того, чтобы их использовать, можно рассматривать как своего рода паранойю. Джозеф Келлер как-то заметил, что в его университете (Стэнфорде) математический факультет имел меньше компьютеров, чем любой другой факультет, в том числе факультет французской литературы. Те математики, которые отказались признать работу Хакена и Аппеля, не могли отрицать, что все математики соглашались принимать традиционные доказательства, даже если они сами не проверяли их. В случае доказательства Великой теоремы Ферма, представленного Уайлсом, менее 10 % специалистов по теории чисел полностью понимали его рассуждения, но все 100 % сочли, что доказательство правильное. Те, кто не смог до конца понять все тонкости доказательства, приняли его потому, что доказательство признали другие—те, кто все понял, шаг за шагом проследил весь ход доказательства и проверил каждую деталь.

Еще более ярким примером может служить так называемое доказательство классификации конечных простых групп, состоящее из 500 отдельных работ, написанных более чем сотней математиков. Говорят, что полностью разобрался в этом доказательстве (общим объемом в 15000 страниц) один-единственный человек на свете — скончавшийся в 1992 году Дэниэл Горенстейн. Тем не менее, математическое сообщество в целом могло быть спокойным: каждый фрагмент доказательства был изучен группой специалистов, и каждая строка из 15000 страниц была десятки раз проверена и перепроверена. Что же касается проблемы четырех красок, то с ней дело обстояло иначе: она никем не была и не будет полностью проверена.

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

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

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

Математик Рональд Грэхем описывает недостаточную глубину компьютерных доказательств на примере одной из великих не доказанных по сей день гипотез — гипотезы Римана: «Я был бы весьма и весьма разочарован, если бы можно было подключиться к компьютеру, спросить у него, верна ли гипотеза Римана, и получить в ответ: "Да, верна, но Вы не сможете понять доказательство"». Математик Филип Дэвис, похожим образом отреагировал на решение проблемы четырех красок: «Моей первой реакцией было: "Потрясающе! Как им удалось решить эту проблему?". Я ожидал какой-то блестящей новой идеи, красота которой перевернула бы всю мою жизнь. Но когда я услышал в ответ: "Они решили проблему, перебрав тысячи случаев и пропустив все варианты один за другим через компьютер", — меня охватило глубочайшее уныние. Я подумал: "Значит, все сводилось к простому перебору, и проблема четырех красок вовсе не заслуживала названия хорошей проблемы"».


Доказательства на чипах | Великая Теорема Ферма | Заслуженная награда