it was the first result at the time from: http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename...
There was a feeling reading the original paper of "why has no one done this yet" but I don't have the chops to ask that, yet.
So in summary: it's hard to prevent, but we're doing our best.
- Is there a limit on the size of the conjecture/formula?
- Would it be viable to use this method (or something similar) for faster formal software verification?
- 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.
sort of spamming number theory at theorems? by discovering a corpus' bias?
Is it safe to say that the architecture in this paper captures MML syntax and the "bounds" within which the software operates?
Hopefully, this will allow automatically proving some of unproven theorems.