Доказательные вычисления

Доказательные вычисления — целенаправленные вычисления на ЭВМ, комбинируемые с аналитическими исследованиями, которые приводят к строгому установлению новых фактов и доказательству теорем.

Достоверные вычисления

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

Примеры

В теории чисел

Благодаря тому, что теория чисел во многом оперирует целыми числами, использование доказательных вычислений в теории чисел оказывается очень плодотворным.

• Утверждается, что число Мерсенна $M_{43112609}=2^{43112609}-1$ является простым. Проверить этот факт теоретически возможно человеку, но практически только с использованием вычислительной техники.
• Л. Эйлер выдвинул гипотезу, что уравнение $x_{1}^{5}+x_{2}^{5}+x_{3}^{5}+x_{4}^{5}=x_{5}^{5}$ не имеет решений в целых положительных числах. Однако позднее было показано, что существует как минимум одно решение:

$x_{1}=27$, $x_{2}=84$, $x_{3}=110$, $x_{4}=133$, $x_{5}=144$.

Причем это решение было найдено с помощью перебора на компьютере.

В теории графов

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

В гидродинамике

Применением доказательных вычислений в математических задачах гидродинамики систематически занимались в Институте прикладной математики им. М. В. Келдыша РАН под руководством К. И. Бабенко. Примером является следующая теорема, полученная с помощью доказательных вычислений.

Теорема. При $\alpha =1.02$ и $R=6000$ спектральная задача Орра — Зоммерфельда имеет собственное значение, лежащее в полуплоскости $\mathrm {Re} \,\lambda >0$. Следовательно, в линеаризованной постановке при этих параметрах течение Пуазёйля неустойчиво.

Ещё примеры

• Задача Буля о пифагоровых тройках.
• Классификация многогранников Джонсона.

См. также

• Математическое доказательство
• Экспериментальная математика

Ссылки

• Интервальный анализ и его приложения

Литература

• Панков П.С. Доказательные вычисления на электронно-вычислительных машинах. — Фрунзе: Илим, 1978. — 179 с.
• К. И. Бабенко. О доказательных вычислениях и математическом эксперименте на ЭВМ // УМН. — 1985. — Т. 40, № 4(244). — С. 137—138.
• Бабенко К. И., Петрович В. Ю., Рахманов А. И. О доказательном эксперименте в теории поверхностных волн конечной амплитуды // Докл. АН. . — 1988. — Т. 303, № 5. — С. 1033—1037.