Как пытаются подходить к автоматическому доказательству теорем с помощью ИИ?

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

Существует Metamath, где формализованы доказательства ~38к утверждений в математике, опираясь друг на друга, и в конечном счёте на базовые аксиомы.

Все доказательства теорем в Metamath базируются на подстановке - это когда мы применяем аксиому или уже доказанную ранее теорему к имеющимся "объектам", чтобы сгенерировать новое промежуточное утверждение. И так, пока не дойдём до теоремы. Этот подход называется forward manner.

Нас же интересует backward manner - это когда у нас есть доказываемое утверждение, и мы применяем к нему тактику, то есть предполагаем, какие промежуточные утверждения, при применении какой-нибудь аксиомы или теоремы, доказали бы желаемое.
Пример: чтобы доказать, что A=C, мы должны доказать, что A=B и B=C, и потом применить транзитивность. Теперь пытаемся доказать, что A=B и B=C.

Таким образом, в backward manner процесс доказательства - это построение дерева.
У каждого утверждения есть дети-тактики - попытки по-разному декомпозировать его на более базовые. И у каждой тактики есть дети-утверждения, все из которых мы должны доказать. Если какая-то вершина оказывается аксиомой или уже доказанным утверждением, то она автоматически доказана. Соответственно, шаг поиска это добавление тактики-ребёнка вместе с его детьми-утверждениями к уже существующей вершине. Это всё похоже на настольную игру. См. картинку.

Буду рад, если математики в комментариях подскажут, какой по сложности является эта задача, если решать её перебором.

А в следующих постах я расскажу о том, как поиск доказательств теорем ускоряют с помощью нейросетей, насколько плохо пока получается, и подумаем над фундаментальными причинами.

@knowledge_accumulator