Доказові обчислення — цілеспрямовані комп'ютерні обчислення, комбіновані з аналітичними дослідженнями, які призводять до строгого встановлення нових фактів і доведення теорем.
Достовірні обчислення Одним із часто застосовуваних методів доказових обчислень є достовірні обчислення. Під достовірними обчисленнями мають на увазі чисельні методи з автоматичною верифікацією точності одержуваних результатів. Досить часто доказові обчислення будуються на основі інтервального аналізу, де замість дійсних чисел розглядаються інтервали, які визначають точність величин. Інтервальний аналіз широко застосовується для обчислень з гарантованою точністю в умовах машинної арифметики.
Приклади
У теорії чисел Завдяки тому, що теорія чисел багато в чому оперує цілими числами, використання доказових обчислень у теорії чисел виявляється дуже плідним.
Стверджується, що число Мерсенна є простим. Перевірити цей факт теоретично може людина, але практично — лише з використанням обчислювальної техніки. Л. Ейлер висунув гіпотезу, що рівняння не має розв'язків у цілих додатних числах. Проте пізніше було показано, що існує принаймні один розв'язок:
, , , , .
Причому цей розв'язок знайдено шляхом перебору на комп'ютері.
У теорії графів Одним з найвідоміших успішних застосувань доказових обчислень у теорії графів є розв'язання проблеми чотирьох фарб. Цю відому задачу поставлено 1852 року і сформульовано так: «з'ясувати, чи можна кожну розташовану на сфері карту розфарбувати чотирма фарбами так, щоб будь-які дві ділянки, які мають спільну межу, були розфарбовані в різні кольори». 1976 року і за допомогою доказових обчислень показали, що так можна розфарбувати будь-яку карту.
У гідродинаміці Застосуванням доказових обчислень у математичних задачах гідродинаміки систематично займалися в Інституті прикладної математики ім. М. В. Келдиша РАН під керівництвом . Прикладом є така теорема, отримана з допомогою доказових обчислень:
Теорема. При і спектральна задача Орра — Зоммерфельда має власне значення, яке лежить у півплощині . Отже, в лінеаризованій постановці за цих параметрів течія Пуазейля нестійка.
Ще приклади Проблема трійок Буля — Піфагора. Класифікація багатогранників Джонсона.
Див. також Доведення Експериментальна математика
Примітки
Література
Посилання Інтервальний аналіз та його застосування