Premise selection with neural networks and distributed representation of features

Andrzej Stanisław Kucik, Konstantin Korovin

We present the problem of selecting relevant premises for a proof of a given statement. When stated as a binary classification task for pairs (conjecture, axiom), it can be efficie…