Доказові обчислення

Завдяки тому, що теорія чисел багато в чому оперує цілими числами, використання доказових обчислень у теорії чисел виявляється дуже плідним.

• Стверджується, що число Мерсенна ${\displaystyle M_{43112609}=2^{43112609}-1}$ є простим. Перевірити цей факт теоретично може людина, але практично — лише з використанням обчислювальної техніки.
• Л. Ейлер висунув гіпотезу, що рівняння ${\displaystyle x_{1}^{5}+x_{2}^{5}+x_{3}^{5}+x_{4}^{5}=x_{5}^{5}}$ не має розв'язків у цілих додатних числах. Проте пізніше було показано, що існує принаймні один розв'язок:

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

Причому цей розв'язок знайдено шляхом перебору на комп'ютері[1].

Одним з найвідоміших успішних застосувань доказових обчислень у теорії графів є розв'язання проблеми чотирьох фарб. Цю відому задачу поставлено 1852 року і сформульовано так: «з'ясувати, чи можна кожну розташовану на сфері карту розфарбувати чотирма фарбами так, щоб будь-які дві ділянки, які мають спільну межу, були розфарбовані в різні кольори». 1976 року К. Аппель і В. Гакен за допомогою доказових обчислень показали, що так можна розфарбувати будь-яку карту.

Застосуванням доказових обчислень у математичних задачах гідродинаміки систематично займалися в Інституті прикладної математики ім. М. В. Келдиша РАНпід керівництвом К. І. Бабенка. Прикладом є така теорема, отримана з допомогою доказових обчислень[3]:

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

• Проблема трійок Буля — Піфагора.
• Класифікація багатогранників Джонсона.