Физика для абитуриента. Математика для физика
Математика для физика. Куда движется математика?
О сайте
Порядок работы
Новости сайта
Контакт
Приёмная комиссия.
Вступительное задание.
Открытые уроки.
Учебники по физике.
Задачи по физике.
Справочник по физике.
Вопросы и консультации.
Рефераты.
Олимпиады и турниры.
Современная физика.
Весёлая наука.
Уголок крохобора.
Не только физика.
Директория ссылок.
Репетиторы
Малая академия наук.
Математика для физика.

Форум.

info@abitura.com

Математика для физика
Пишите...

Куда движется математика?

Брайан Дэвис ( Brian Davies ),
профессор математики Лондонского Королевского Колледжа

•  Введение

•  Доказательства с использованием компьютера

•  Формальная проверка доказательств

•  Простые конечные группы

•  Непротиворечивость арифметики

•  Обсуждение

•  Ссылки

 

Доказательства с использованием компьютера

Первым примером крупной математической теоремы, для доказательства которой был применен компьютер, стала теорема о четырех цветах, доказанная в 1976 году Аппелом и Хакеном [1], [2]. Это сильно обеспокоило многих математиков по двум причинам. Во-первых, был выдвинут довод, что в корректности доказательства невозможно убедиться , не перепроверив вручную все итерации расчетов, проделанных машиной. На тот момент доказательства «правильных» теорем еще казались практически всем математикам безупречными. Возможность случайных ошибок в доказательствах признавалась, но их исправление считалось делом времени. Другое дело, что уже тогда некоторые математики стали задумываться не над тем, истинна ли та или иная теорема, а над тем, почему она считается истинной. Доказательства без понимания сути их не интересовали.

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

Задача Кеплера заключается в поиске наиболее компактного варианта упорядочивания твердых сферических тел равного диаметра в трехмерном объеме с целью получить максимальную среднюю плотность его заполнения. Ожидаемое решение известно уже давно и широко практикуется на прилавках с апельсинами, выложенными горкой. В 1998 году Том Хейлз объявил о найденном им строгом математическом решении задачи Кеплера, основанном на сочетание аналитической геометрии и сложных компьютерных вычислений. Журнал «Анналы математики» принял статью на экспертизу и созвал комиссию из двадцати ведущих специалистов в этой области, чтобы они дали отзыв о статье. Экспертная комиссия начала свою работу с конференции в Принстонском университете по выработке общей стратегии. Шли годы, референты постепенно выходили из состава комиссии, и наконец в начале 2004 года было окончательно решено отказаться от усилий рецензировать статью. Редколлегия журнала решила опубликовать «теоретическую часть» работы, а «компьютерную часть» переадресовать в какой-нибудь более подходящий журнал. Член редколлегии «Анналов» Роберт Макферсон по этому случаю заметил, что «в отношении статей подобного рода (негласные) редакционные правила отбора материалов к публикации просто не работают» [18].

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

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

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

Из положительных сторон я должен все-таки отметить, что компьютеры значительно разгрузили чистых математиков от нудных рутинных расчетов. Вот лишь несколько наугад взятых примеров, которые можно подразделить на несколько категорий. Компьютерная алгебра позволяет быстро производить безнадежно долгие в иных случаях вычисления, необходимые во многих областях знания. Статистическая физика, изучающая динамику поведения макросистем, состоящих из огромного набора хаотически движущихся частиц, не могла бы достичь современного уровня развития без возможности проведения колоссального количества числовых экспериментов. Да, верно, неупорядоченный характер движения тепловых частиц был открыт Анри Пуанкаре еще в конце XIX века; но так же верно и то, что прогрессом статистической физики мы во многом обязаны развитию компьютерных технологий. Невероятная разница в спектральных характеристиках самосопряженных и несамосопряженных матриц была выявлена именно благодаря численным методам и привела к развитию совершенно новой области псевдоспектрального анализа, который сегодня справедливо считается самостоятельным и полноправным разделом «строгой математики» [28].

Контролируемые численные методы сегодня играют важнейшую роль и в статьях, посвященных проблемам чистой математики. В некоторых областях, в частности в области нелинейных дифференциальных уравнений высокого порядка, только компьютерные методы позволили доказать существование решений [22], [23]. При этом в расчетах использовались стандартные итерационные методы и методики расчета допустимых ошибок и доверительных интервалов, принципиальную правильность которых сегодня никто не оспаривает. Главное — строгое доказательство неравенства, которое затем становится неотъемлемой частью доказательства теоремы. В принципе, все те же расчеты можно было бы проделать и вручную, только вот на практике такие трудозатраты оказываются нереальными.

<<Назад  |  Дальше>>


О сайте
Порядок работы
Новости сайта
Контакт

Вверх .

Главная страница .

Rambler's Top100Rambler's Top100