This is fascinating. If i had more time to get an articulate question i would, but I'm going to need to sit with this paper for a bit. Amazingly, I've been fooling around on the edges of thereom proving for a bit now and had yet to hear of the Mizar corpus. Really, really fascinating stuff.
How do you avoid accidently encoding knowledge into your algorithm? You can't test your algorithm on a different sample of naturally occurring mathematics , summer wet have only one.
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.
- 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.
so you're limiting the scope of potential solutions to theorems and then trying to eventually supplant a brute force method with biologically informed cognitive methods? neural networks?
sort of spamming number theory at theorems? by discovering a corpus' bias?
