Доказательные вычисления — целенаправленные вычисления на ЭВМ, комбинируемые с аналитическими исследованиями, которые приводят к строгому установлению новых фактов и доказательству теорем.
Достоверные вычисления Одним из часто применяемых методов доказательных вычислений являются достоверные вычисления. Под достоверными вычислениями понимаются численные методы с автоматической верификацией точности получаемых результатов. Довольно часто доказательные вычисления строятся на основе интервального анализа, где вместо вещественных чисел рассматриваются интервалы, которые определяют точность величин. Интервальный анализ широко применяется для вычислений с гарантируемой точностью в условиях машинной арифметики.
Примеры
В теории чисел Благодаря тому, что теория чисел во многом оперирует целыми числами, использование доказательных вычислений в теории чисел оказывается очень плодотворным.
Утверждается, что число Мерсенна является простым. Проверить этот факт теоретически возможно человеку, но практически только с использованием вычислительной техники. Л. Эйлер выдвинул гипотезу, что уравнение не имеет решений в целых положительных числах. Однако позднее было показано, что существует как минимум одно решение: , , , , . Причем это решение было найдено с помощью перебора на компьютере.
В теории графов Одно из наиболее известных успехов применения доказательных вычислений в теории графов является решение проблемы четырёх красок. Эта знаменитая задача была поставлена 1852 году и формулируется следующим образом: «выяснить, можно ли всякую расположенную на сфере карту раскрасить четырьмя красками так, чтобы любые две области, имеющие общий участок границы, были раскрашены в разные цвета». В 1976 году К. Аппель и В. Хакен с помощью доказательных вычислений показали, что так можно раскрасить любую карту.
В гидродинамике Применением доказательных вычислений в математических задачах гидродинамики систематически занимались в Институте прикладной математики им. М. В. Келдыша РАН под руководством К. И. Бабенко. Примером является следующая теорема, полученная с помощью доказательных вычислений.
Теорема. При и спектральная задача Орра — Зоммерфельда имеет собственное значение, лежащее в полуплоскости . Следовательно, в линеаризованной постановке при этих параметрах течение Пуазёйля неустойчиво.
Ещё примеры
Задача Буля о пифагоровых тройках. Классификация многогранников Джонсона.
См. также Математическое доказательство Экспериментальная математика
Примечания
Ссылки Интервальный анализ и его приложения
Литература
Категория:Вычислительная математика Категория:Автоматическое доказательство теорем