Одно из старейших направлений в искусственном интеллекте — автоматическое доказательство теорем. Важность его очевидна — если научить машину без участия человека доказывать теоремы, то потом можно будет автоматизировать процесс формулировки теорем. Можно будет перепроверить справедливость уже доказанных теорем, пересчитать все теоремы и систематизировать. Правда до этого еще далеко, хотя Wolfram Alpha уже сейчас научилась доказывать методом математической индукции справедливость математических соотношений. А это уже заявка на массовое использование математического аппарата доказательств. Можно теперь быстро и просто без специальных знаний одной командой проверить справедливость того или иного утверждения. Но, пора переходить к примерам.
Все помнят еще со школы известную формулу для нахождения суммы n-натуральных чисел:
Чтобы проверить справедливость этой формулы достаточно отправить команду:
В результате получим подтверждение справедливости формулы.
Следующий пример показывает случай, когда утверждение не будет верным. Например, мы решили проверить будет ли выражение 8^n-3^n делиться на число 12 для всех n>0. Следующая команда легко позволяет это утверждение проверить, точнее получить подтверждение его ошибочности:
Теперь любая домохозяйка может придумать формулу и легко, как на калькуляторе ее доказать или опровергнуть. И это только начало...