Josef Urban†

Large formal mathematical knowledge bases en-code considerable parts of advanced mathematics and exact science, allowing deep semantic com-puter assistance and verification of complicated theories down to the atomic logical rules. An es-sential part of automated reasoning over such large theories are methods learning selection of relevant knowledge from the thousands of proofs in the cor-pora. Such methods in turn rely on efficiently com-putable features characterizing the highly struc-tured and inter-related mathematical statements. In this work we (i) propose novel semantic features characterizing the statements in such large seman-tic knowledge bases, (ii) propose and carry out their efficient implementation using deductive-AI data-structures such as substitution trees and discrimina-tion nets, and (iii) show that they significantly im-prove the strength of existing knowledge selection methods and automated reasoning methods over the large formal knowledge bases. In particular, on a standard large-theory benchmark we improve the average predicted rank of a mathematical statement needed for a proof by 22 % in comparison with state of the art. This allows us to prove 8 % more theo-rems in comparison with state of the art