DeepMath – Deep Sequence Models for Premise Selection

- the most interesting thing about this approach is that it managed to prove a significantly different set of theorems than previous state-of-the-art approaches. So theorems that are hard to prove for this approach were not all hard to prove for previous approaches, and inversely this approach can prove theorems that were hard for previous approaches.

- in this specific setup, yes, all sequences are truncated for practical reasons. In theory there should be no size limit, however long sequences will of course be more difficult to meaningfully encode.

- formal software verification is definitely one of the long-terms goals of this project. I think software verification is one of the big challenges of our transition into an information society (as algorithms/AI start having more control over our lives, as we start using smart contracts, etc), and AI will help solve it. The current setup would not be of much help, however.

You should read https://intelligence.org/2013/12/21/josef-urban-on-machine-l... and the citations! After that, you almost wonder why no one had applied NNs before.

Information leaks are indeed the number one challenge when evaluating this type of approach. Our evaluation procedure does not rigorously guarantee against information leaks, but it does allow for an apples-to-apples comparison with previous methods (which had the same potential issue). And showing an advantage over these methods is what we were trying to achieve.

So in summary: it's hard to prevent, but we're doing our best.