Note that it's not obvious at all how to search the space of possible exotic identities, so a potential direction for future work would be to have a loop in which LLMs (perhaps through something like AlphaEvolve) propose an exotic identity, and then a SAT call tries to find a small countermodel. A big issue though, is that even with our efficient encoding the SAT calls would take at least a few minutes, so we wouldn't be able to afford testing millions of candidates. But if there were 1000 candidates that could potentially be tested...
(I'm one of the authors of the paper, thanks for the coment!).
I wish you spent at least a couple words in the paper about that. Even negative results are worth documenting! (even if you didn't get up to size 11, I'd've loved to hear about those other alternatives)
---
by the way, you mentioned that decreasing HSI6/10 from O(n^6) to O(n^5) clauses was slower - how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?
---
also, have you tried reordering order of operations in symmetry break? how much did it affect the search? I wonder if unique multiplication table might've been of help had it been disambiguated stronger (or weaker)
Tarski said "hey, what if we limit ourself only to positive integers? subtraction/division doesn't always work, so let's get rid of it. What can we say about +^? there are some obvious properties, like x+y=y+x for whatever x and y. Is that enough to describe all the equalities?".
Wilkie answered No, and a whole different hunt began - trying to find a set of pseudo "numbers" with pseudo "+^", that would have the same obvious properties, but not the non-obvious one
and SAT-solving is essentially asking computer to find things by describing what they are not - "1+2 is not invalid and can't be 2 different values", "1+(1+1) must not differ from (1+1)+1". A lot of such properties are easily expressible as "not the opposite" - but devil's in the details and some choices of opposites are faster for computer than others. Also symmetries are evil :)