Is it plausable that all remaining implications are false?

Stream: Equational

[Daniel Weber]

There are some peculiar experimental results I'm getting, which make me suspect that all (or almost all) remaining implications are false. Essentially, they are "Vampire can prove all true implications I know of in <0.05s, and running it with a time limit of 5 seconds there are no further implications it can prove." Another explanation, of course, is that there is some kind of huge gap between "easy" implications and "hard" implications, but it feels to me like that makes less sense

[Terence Tao]

I'm hoping a run of linear magmas may clarify things further. From the few data points we have it seems that many remaining implications are in fact easily refuted by linear magmas, they were simply missed in the earlier quadratic runs because linear laws are too sparse a subset of the quadratic laws.

The hardest positive implication I know of was 1689 -> 2. How long does this take on Vampire? Are there any other ones that take Vampire even longer?

[Zoltan A. Kocsis (Z.A.K.)]

Another explanation, of course, is that there is some kind of huge gap between "easy" implications and "hard" implications, but it feels to me like that makes less sense

I am not at all convinced. Vampire is pretty much the state-of-the-art in first-order theorem proving, and has been for a while. It can establish a lot of easy stuff quickly. And yet, year-by-year, CADE comes up with easy problems that it can't solve (and sometimes older not SoTA provers, like Prover9, can! This happened in e.g. 2020.)

Moreover, Prover9 used to be state-of-the-art too. This project could have started back then, and then we would actually see the graph split into faux "easy" and "hard" implications, with Prover9 handling the "easy" ones quickly, and the hard ones not at all!

I think e.g. 65 might imply 3862. It's easy to prove that there are no finite counterexamples, and while I didn't give it more than 30 mins of thought, I had a hard time imagining what infinite counterexamples could look like.

[Daniel Weber]

Terence Tao said:

I'm hoping a run of linear magmas may clarify things further. From the few data points we have it seems that many remaining implications are in fact easily refuted by linear magmas, they were simply missed in the earlier quadratic runs because linear laws are too sparse a subset of the quadratic laws.

The hardest positive implication I know of was 1689 -> 2. How long does this take on Vampire? Are there any other ones that take Vampire even longer?

It takes 0.05s. I had a histogram somewhere, but I can't find it now. I'll try to search again

[Terence Tao]

It might be fun to publish a list of Vampire-hard implications on the web page. With a link to a lean playground to challenge humans to solve them. UPDATE: proposed at equational#370

[Daniel Weber]

Once we add stuff Vampire can disprove but we can't formalize yet as conjectures that should be possible in the equation explorer

[Will Sawin]

How stable is vampire under adding additional binary operations? To me after pondering the problem of whether 65 implies 3862 it seemed like it was clearer if you express 65 as two equations in two binary operations *, o given by y * (y o x) =x and y o x = x * (y * x) (where o is the original one). Could that possibly affect the difficulty of a proof or disproof?

[Daniel Weber]

It doesn't seem to help

[Zoltan A. Kocsis (Z.A.K.)]

As a general rule, additional symbols tend to hinder instead of help the current generation of ATPs (you can engineer exceptions, of course). Indeed, some include heuristics specifically to detect and eliminate operations that are definable from others.