Cluster in the refutations data

Stream: Equational

[Vlad Tsyrklevich]

In the data Nicholas generated, I calculated the number of outbound and inbound not-implies for every equation. (It's here if anyone wants to look https://gist.github.com/vlad902/e784b4dbca1457ba75cdec259bad2b7b) Unsurprisingly, the equations I found that imply each other (ref https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Outstanding.20tasks.2C.20v1/near/473229484), have the same inbound/outbound counts. Here are the top clusters by how often they occur and their inbound,outbound count:

 121 4119,2913
 123 4119,2988
 152 3480,3034
 419 3138,2767
1508 0,3186

I found it interesting how many equations clustered into the same inbound/outbound counts. This could very well be an artifact of having a finite number of formulas, but for formulas that I looked at, the equations do look structurally related.

The largest cluster, is 1508 equations that no-imply 0 equations, but are not-implied by all the other 3186 equations. This is the cluster consisting of Equations 2, 6, 7, 15, 17, etc. In my data counting trivial implications, this cluster of 1508 equations all are implied by other formulas in the cluster except for Equation 2 at the root. If I understand it correctly, none of the Equations in this cluster are realizable for magmas of size >1, so it seems like there should be a proof that all are impossible to generate (for size >1) and hence equivalent, instead of the weaker implications I am generating by manipulating rewrites.

[Daniel Weber]

It might be interesting to compute the automorphism group of the refutation graph, I think a graph of this size should be doable by nauty

[Amir Livne Bar-on]

There are easy proofs for most of this cluster. I'm pushing soon a PR with 815 of them, hopefully this will help us avoid wasting computation time on them in the future.

[Amir Livne Bar-on]

That is, proofs of the form EqX => Eq2, which IIUC aren't covered by the rewriting technique