premise-selection-nn

Premise selection model using artificial neural networks. It requires the data collected and formated by Josef Urban (https://github.com/JUrban/deepmath/tree/master/nndata) to form training and test conjecture-axiom pairs. The parser and lexer are written using Lark (https://github.com/erezsh/lark).