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

Может ли компьютер доказать теорему?

Обсудить
Может ли компьютер доказать теорему?
Источник:

Legion Media

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

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

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

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

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

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

Подписываясь на рассылку вы принимаете условия пользовательского соглашения