Почему компьютеру так сложно что-то доказать?

Это можно считать глупым вопросом. Я не специализируюсь в области компьютерных наук (и еще не изучаю математику), поэтому, пожалуйста, извините, если вы считаете, что следующие вопросы отражают некоторые ошибочные предположения.

Хотя есть планы формализовать последнюю теорему Ферма (см. Эту презентацию ), я никогда не читал и не слышал, что компьютер может доказать даже «простую» теорему, подобную Пифагору ».

Почему нет? Что является (/ являются) главной трудностью (-ями) позади создания полностью автономного доказательства с помощью компьютера, которому помогают только некоторые "встроенные аксиомы"?

Второй вопрос, который я хотел бы задать, заключается в следующем: почему мы можем формализовать множество доказательств, хотя в настоящее время компьютер не может доказать теорему самостоятельно? Почему это "сложнее"?

Хотя есть планы формализовать последнюю теорему Ферма (см. Эту презентацию), я никогда не читал и не слышал, что компьютер может доказать даже «простую» теорему, подобную Пифагору ».

В 1949 году Тарский доказал, что почти все в Элементах лежит в разрешимом фрагменте логики, когда он показал разрешимость теории первого порядка реальных замкнутых полей. Так что теорема Пифагора, в частности, мало о чем говорит, потому что она не особенно сложна.

Вообще, вещь, которая делает доказательство теоремы, является индукцией. Логика первого порядка без индукции обладает очень полезным свойством, называемым свойством субформулы : истинные формулы имеют доказательства, включающие только подтермы $A$$A$ . Это означает, что можно построить доказатели теорем, которые могут решить, что доказывать дальше, на основе анализа теоремы, которую они должны доказать. (Создание экземпляра квантификатора может сделать правильное понятие подформулы более тонким, но у нас есть разумные методы, чтобы справиться с этим.)

$A$$B$$A$

Две основные трудности. Неполнота (см. Теоремы Гёделя о неполноте) и огромный размер пространства поиска (там гораздо больше неинтересных теорем, чем интересных). Значительный прогресс был достигнут с использованием корректоров ( Coq , Isabelle, Agda и т. Д.). С их помощью математик пишет теоремы и леммы, а помощник по доказательствам помогает находить доказательства и обеспечивает их логическую обоснованность.

$P$$Q$$P\wedge Q$ . Конечно, если процедура поиска более умна, вы можете обнаружить более умные вещи, но чтобы найти что-то действительно интересное и оригинальное, потребовалось бы много умных приемов и приемов со стороны программиста. Теоремы Гёделя о неполноте актуальны здесь, потому что они налагают фундаментальное ограничение на то, что может быть обнаружено в любой системе доказательств: компьютер никогда не сможет обнаружить доказательство непротиворечивости своей собственной логики.

Эта статья описывает, как помощник по доказательству Coq используется для доказательства теоремы о четырех цветах. Механизированная математика ( обзор ) - это одна из областей TCS, посвященная (полу) автоматическому доказательству теорем (и вообще использованию компьютеров для помощи математикам).

Одной из областей, в которых автоматизированное доказательство теорем (своего рода) оказывает влияние, является проверка моделей и поиск моделей. Проверка модели имеет дело с определением, удовлетворяет ли данная система заданному свойству, тогда как поиск модели находит систему, которая удовлетворяет заданному набору свойств. Инструмент Alloy использует проверку моделей и поиск моделей с хорошим эффектом, и он вполне пригоден для использования.