Иногда может, но обычно лишь ассистирует в этом человеку
На самостоятельное доказательство теорем была способна еще программа «Логик-теоретик», написанная в 1956 г. Причем иногда она находила более краткое и изящное доказательство, чем известное человеку.
А может ли компьютер доказать совершенно новую теорему, еще не доказанную ни одним математиком? И такое случается, хотя и очень редко. Пример — доказательство гипотезы Роббинса (всякая алгебра Роббинса является булевой).
И все же обычно умозаключениями занимается человек, а компьютеру остается рутинная работа. Например, есть программы для проверки готовых доказательств на логические ошибки.
Важный пример использования компьютера связан с теоремой о четырех красках. Она гласит, что любую плоскую карту можно покрасить в четыре цвета так, что никакие две соседние страны не будут одноцветными. Можно рисовать страны любых размеров и форм, так что всевозможных карт бесконечно много.
Но в 1976 г. Кеннет Аппель и Вольфганг Хакен показали, что любая карта может быть сведена к одному из 1936 частных случаев. Компьютер перебрал все эти случаи, и на этом доказательство было завершено. Сегодня уже многие теоремы доказаны таким способом.
