Refutations with finite cancellative magmas

Stream: Equational

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

Hello everyone,

A cancellative magma satisfies both $xy=xz \rightarrow y=z$ and $yx=zx \rightarrow y=z$. These magmas are simpler to list than all magmas, as there's a lot fewer of them. Specifically, there are only 1410 distinct 5x5 cancellative magmas (up to isomorphism), and Mace4 can generate all of them in under 20 seconds. A shell script to do this is available here.

Adding the 5x5 cancellative magmas to the existing 2x2-4x4 exhaustive dataset helps disprove more "potential implications" than using only the 2x2-4x4 dataset.

By experimenting with Mace4 manually, I also found 8 larger cancellative monoids that refuted even more implications. Eventually, I was able to compile a shortlist of 515 magmas (from 2x2 to 8x8) which refuted 13842823 potential implications, which is about 100,000 more than the 2x2-4x4 dataset could do (and includes all the ones that the 5x5 cancellatives list refutes, ofc).

This shortlist is here in a format similar to @Nicholas Carlini 's original 4x4 outputs.

The list above was created by a Haskell script I wrote, which generates optimized proof plans from lists of finite magmas and the equations they satisfy, based on a cost model. The aim is to minimize the number of large identities that the Lean kernel has to verify, while still covering all the counterexamples provided by the list.

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

I wrote another Haskell script that generates Refutation<n>.lean files, similar to those in used by @Joachim Breitner in the all4x4lean branch.

With these files, I could run verification on a fork of that branch, and the proof works (quite quickly, considering there are 515 magmas). I haven't tried pruning based on transitivity yet (and I'm unsure how to approach that, so any guidance would be helpful), but it should reduce the number of checks further.

What's the next step?

• I think this should be integrated with All4x4Tables instead of creating a new directory (otherwise, there'd be a lot of redundancy). How should I structure this, and what issues or PRs should I create? I haven't contributed to large Lean projects before, so I don't really know the typical workflow. Please bear with me.

• I developed several Haskell tools for this, currently available here These include tools to parse Mace4 output, the proof-planning script, etc. I think others might find them useful, but Haskell is quite heavy and needs to be built with cabal. Should I still try to eventually get this into the upstream scripts/ folder, or is it better if I just leave them in my own fork for now?

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

Another thing: a peek at OEIS suggest there should be 1130531 cancellative magmas of order 6 up to isomorphism. So it might be possible to evaluate them all with the aid of Mace4 or SMT solvers. Not sure if it's worth doing - I doubt that cancellative magmas will satisfy many remaining equations of interest.

[Nicholas Carlini]

Very nice! The CONTRIBUTING file has some steps for what to do for automated proofs. Briefly:

• Add the code to Generated/[place]/src
• Put a few steps for how to run it
• Maybe add to the blueprint
• And maybe update the README

I think putting in the 4x4 would be okay, we should probably rename it anyway because it will soon also be 2x2 and 3x3.

[Joachim Breitner]

We have various efforts that produce small counterexamples, for example see my review here:
https://github.com/teorth/equational_theories/pull/103#pullrequestreview-2343208947

I think it would make sense to define a common simple text format for finite magmas, something like

{ "size": 4, "table": [[3, 3, 2, 3], [3, 3, 2, 3], [0, 0, 2, 0], [3, 3, 2, 3]], "satisfies": [1, 307, 309, 323, 326, 329, 359, 364, 375, 385, 395, 3253, 3255, 3258, 3261, 3264, 3306, 3309, 3312, 3316, 3319, 3322, 3326, 3330, 3334, 3338, 3456, 3458, 3461, 3464, 3467, 3509, 3512, 3515, 3519, 3522, 3525, 3529, 3533, 3537, 3541, 3659, 3661, 3674, 3677, 3680, 3712, 3715, 3718, 3749, 3752, 3755, 3786, 3790, 3794, 3798, 3862, 3867, 3877, 3887, 3897, 3915, 3925, 3935, 3952, 3962, 3972, 3989, 4006, 4023, 4040, 4065, 4070, 4080, 4090, 4100, 4118, 4128, 4138, 4155, 4165, 4175, 4192, 4209, 4226, 4243, 4269, 4284, 4287, 4316, 4340, 4360, 4380, 4385, 4396, 4406, 4416, 4432, 4442, 4452, 4470, 4480, 4490, 4508, 4525, 4542, 4559, 4587, 4606, 4615, 4645, 4666, 4689], "tested_up_to": 4906 }

this is similar to what Nicholas genererates. The tested_up_to is shorter than listing the refuted ones, while being future-proof if we ever extend the list of equations.

Then there is a single script that reads these files and creates lean proofs from that, also taking known implications into account.

There is no need to implement the lean-producing script multiple times.

[Nicholas Carlini]

Actually having a datastructure that's shared for these tables would be great. Your version here makes sense for any enumeration over tables.

I'd propose one metadata tag of like type: "table". I think we could use the same general format for, e.g., polynomials and then just instead of having "table": we have "polynomial": [whatever format]

[Joachim Breitner]

I thought we’d just use "poly": "2*x*x + 5" instead of the table field ,and the existence of the field indicates the type, but either is fine.

[Nicholas Carlini]

That could work too, as long as we don't want to share a key and there's a way to uniquely identify which format each line is in. My thought here is it's just less error prone to store the expected type instead of inferring it from what keys are/are not present.

[Joachim Breitner]

Using keys to encode sum types in JSON is common, but an explicit type is fine with me. Whoever implements this format first gets to decide (so not me) :-)

[Terence Tao]

Just a note for future development: I think having a standardized system for accepting large lists of finite magmas is a great idea, and if this happens, one should update CONTRIBUTING.md with a section on how to submit such lists and what standard formats one should use.

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

Joachim Breitner said:

Whoever implements this format first gets to decide (so not me) :-)

Fair, but I guess agreeing on a standard prior to its initial implementation has some benefits: as @Terence Tao points out, it can be included in CONTRIBUTING.md, so

• future contributors will follow the standard rather than invent yet more formats,
• issues can be opened to update current tools to align with the standard.

[Nicholas Carlini]

(I think the comment was just meant to say "both options are reasonable whoever implements it can pick between two good choices" and not "there shouldn't be a good standard")

[Terence Tao]

By the way, I think this discussion falls under the scope of equational#180, and I will link to this thread accordingly.

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

Okay, I've created PR#224 for the 5x5 cancellative magma refutations.

It adds new tools under src/, updates the README with running instructions, and adds new Refutations*.lean files which include the 5x5 and larger magmas.