Magma sampler for given identity

Stream: Equational

[Martin Dvořák]

Is anybody working on the following?

Given a law (an identity) that must be satisfied, generate arbitrary (not necessarily random) nontrivial examples (as many as possible) of finite magmas on >4 elements that satisfy given law. Ideally something that I could seed the table a few values and let it generate the rest so that given identity is satisfied...

[Cody Roux]

Like trying to prove a non implication, getting a negative answer in this case is going to be hard... :)

I'd recommend creating an issue here and then claiming it.

[Martin Dvořák]

Yes, I would like to use it to refute non-implications that have a finite counterexample yet the exhaustive counterexample search is not sufficient for.

[Cody Roux]

I mean asking "is anyone working on X?" can only get positive answers, rarely "no, no one". Like "are you asleep?"

[Cody Roux]

Though I'd make sure the effort at https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Resolving.20.20.3E60.25.20of.20cases.20with.20non-implications.20automatically does not overlap.

[Daniel Weber]

There was some talk about using Z3 to do that, #Equational > Using automated theorem provers might also be relevant

[Nicholas Carlini]

I am not working on this at the moment, but have ideas for something I would like to try to do this. I feel like this direction is likely to be fruitful enough that multiple people working on it simultaneously are likely to produce very different approaches that refute different implications.

[Cody Roux]

I do have the script checked in: https://github.com/teorth/equational_theories/blob/main/scripts/generate_z3_counterexample.py

not sure how usable it is.

[Sebastian Luther]

https://github.com/teorth/equational_theories/pull/103

contains something that goes somewhat in this direction.
It takes an equation and a list of equations as input.
It then searches for a single magma for which the equation is satisfied and as many of the equations in the list are not.
The proofs in there are obsolete and inefficient, but I have an improved version.
I used that to search for equations for which the smallest magma is of size 5 (which are 467,677,704,1076,1279,1313,1516,2091,2294,2328,2531,2903,2910,3140). I'm currently running it to find all non-implications for these equations. I plan to update the PR once that's done.

For your problem: Fixing some values in the table would be easy, but generating as many magmas as possible not so much. Especially because the search is not that fast.