DATA: Create a text file to store interesting finite magmas of size 5 or greater - such as (Z/6Z,+), and automated tools to use this text file to generate anti-implications.

[teorth]

More specifically, create a script to test the magmas in the text file against the list of outstanding implications, and add any anti-implications generated to the list of generated equations. Also, create CI so that if additions are made to the text file, then the script is run again.

Discussion at https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Collecting.20interesting.20finite.20magmas

[carlini]

Note that (Z/6Z, +) and other similar equations should already be included in the set of finite polynomial refutations generated by brute force because it searches over equations of the form ax^2 + by^2 + cx + dy + exy. (This was not completely exhaustive search, but it was pretty close, and I've just checked that nothing new would be implied by it that wasn't already covered by the current polynomials.)

That said: I agree it would be great to collect larger interesting sets of interesting magmas to run brute force that likely weren't covered.

[teorth]

Onh ok. Then Z/6Z can just be used as a test case to check that it doesnt rule out any still open implications, but hopefully people will contribute more interesting finite magmas soon.

[carlini]

In case someone's curious, I believe the following two implications from the finite_poly generations "cover" (x + y) % 6:
(3 * x**2 + 3 * y**2 + 1 * x + 1 * y + 0 * x * y) % 6
and
(0 * x**2 + 2 * y**2 + 0 * x + 2 * y + 3 * x * y) % 4.

[teorth]

The discussion at https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Refutations.20with.20finite.20cancellative.20magmas is also relevant. We should have a standardized system for accepting lists of finite magmas (either small human-generated files or large computer-generated files) in a standard location, so that automated tools can test them for refutations, and update CONTRIBUTING.md to describe the procedures and standards for doing so. Perhaps a system of having unlimited numbers of text files in a standard directory would be a better organizational structure than my original proposal to have a single text file to contain all of the lists.

[teorth]

See the discussion in #294 for a description of the current options to incorporate finite magmas into the automated refutation generator. The main thing currently missing is a user-friendly interface to input them. See also the discussion at https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/using.20z3