Может ли компьютер доказать теорему?
Фото
YAY Media AS / Alamy via Legion Media

Иногда может, но обычно лишь ассистирует в этом человеку

На самостоятельное доказательство теорем была способна еще программа «Логик-теоретик», написанная в 1956 г. Причем иногда она находила более краткое и изящное доказательство, чем известное человеку.

А может ли компьютер доказать совершенно новую теорему, еще не доказанную ни одним математиком? И такое случается, хотя и очень редко. Пример — доказательство гипотезы Роббинса (всякая алгебра Роббинса является булевой).

И все же обычно умозаключениями занимается человек, а компьютеру остается рутинная работа. Например, есть программы для проверки готовых доказательств на логические ошибки.

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

Но в 1976 г. Кеннет Аппель и Вольфганг Хакен показали, что любая карта может быть сведена к одному из 1936 частных случаев. Компьютер перебрал все эти случаи, и на этом доказательство было завершено. Сегодня уже многие теоремы доказаны таким способом.