4×4 magmas

Stream: Equational

[Joachim Breitner]

I just saw that @Nicholas Carlini’s exhaustive data about 4×4 magmas has landed in https://github.com/teorth/equational_theories/pull/150, so PR https://github.com/teorth/equational_theories/pull/172 adds it to lean.

@Nicholas Carlini , how useful are the polynomial based examples now that we have the 4×4? Worth keeping? Worth reducing that dataset to new results?

[Joachim Breitner]

Also, in terms of smaller proofs, could you adjust your 4×4 dump to include 2×2 and 3×3 as well, and first? Presumably that also refutes a fair number of implications, and is faster to check, and that means we have to check fewer 4×4 magmas.

[Nicholas Carlini]

Someone else has already done the 3x3 work. I could generate it too, but let me comment there and see if they want to merge their 3x3 version in first since they brought it up first.

[Joachim Breitner]

I don’t think it makes sense to maintain two separate code bases for the same task (enumerating magmas). The faster implementation of the two should prevail. Also having it all in one refutation.txt (or at least same-format files) makes pruning-while-generating-lean easier.

[Nicholas Carlini]

OK

[Nicholas Carlini]

I'll edit mine to generate 2x2 and 3x3 tables too and submit that, probably tomorrow though.

[Joachim Breitner]

Great, I’ll wait with #172 then until it’s in then, please ping me then.

[Nicholas Carlini]

@Joachim Breitner it's in now, #187

[Joachim Breitner]

Thanks!

[Nicholas Carlini]

It's actually not better

[Nicholas Carlini]

I think I have a bug that's missing some magmas improperly. I don't know why right now, but I should sleep, I have a run going to diagnose.

[Nicholas Carlini]

(Glass half full: either the code is right, or we're going to get a bunch more refutations!)

[Joachim Breitner]

Mind if I merge the leanification of the 4×4 magmas then, so that these results show up? Happy to help adjusting it to more files later, of course.

[Nicholas Carlini]

Of course that's fine yeah. It'll only get better if I find more by brute forcing harder.

[Nicholas Carlini]

It looks like it's unlikely that you'll want to remove any 4x4 magmas from the 3x3 set anyway, if anything you'll want to do the reverse because the 4x4s almost cover the 3x3s but the reverse is not true

[Joachim Breitner]

Unless the 3×3 are so much faster to process (if 333… is much smaller than 44*4…). But yes, just a matter of the order the script looks at the files, so I can just try once they are there.

[Terence Tao]

Are the 4x4 magmas reduced by isomorphism? In principle that offers a roughly 4!=24 speedup after a one time preprocessing.

[Joachim Breitner]

At least the lean proofs we generated are implicit reduced, because we only add those that add new counter-examples, so isomorphic ones are dropped along the way. I don’t think Nichola’s C code tries to avoid isomorphism.

Is this true: If we only look at tables where the first occurrences of elements 1, 2,3 and 4 are in that order, then we look at each isomorphism class once?

[Terence Tao]

I don't think it's that simple, because isomorphism permutes the locations of the table entries as well as the values of the table, so the notion of "first occurence" gets messed up by the isomorphism.

Perhaps the fastest way to enumerate up to isomorphism is to have an dictionary of size 4^{4*4} associated to all 4 x 4 magmas, and enumerate along this dictionary, creating the indicated magma (if the dictionary entry is not already filled), generating its 4!-1=23 permutations (in some cases fewer due to symmetries of the magma), and adding a dictionary entry for each of the permutations indicating that it is a permutation and so can be skipped over when one encounters it the enumeration. This will naturally generate a list of magmas up to equivalence, with each equivalence class represented by its earliest member in the dictionary. This should take roughly 4^{4*4} time and space (each new class requires 4! or so operations, but the number of classes is roughly 4^{4*4}/4!, so it cancels out).

[Terence Tao]

The one catch with this approach is that the memory required is equal to the size 4^{4*4} of the total set of magmas, not the set quotiented out by equivalence. For 4x4 this isn't a serious problem but may be a concern when enumerating larger classes of magmas quotiented out by larger sets of symmetries (e.g., the 5!=120-element group of permutations on five elements). A hash table may be a better solution here, but could require more effort to implement.

[Johan Commelin]

Already $4^{4 \cdot 4}$ will take up ~ 8GB right? If we use 2 bytes for the label of a magma...
So doable, but not something you want to do too often.

[Terence Tao]

Computing the isomorphism classes only has to be done once, and the data file can be deleted afterwards. This data set may also already exist online, for instance one of the links at https://oeis.org/A001329 may already contain it (but I haven't checked).

[Joachim Breitner]

The blueprint says

Sep 29, 2024: 13.7m implications were conjectured to be refused by a collection of 515 magmas, collected by enumerating all 4^(4*4) operators and reducing to a covering set.

but these are proven, aren’t they?

[Nicholas Carlini]

I think they have since been

[Nicholas Carlini]

(I think the status just needs to be updated, since first they were conjectured, then proven)

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

Indeed. The final count is 13.8mil btw (13,842,823 precisely, soon to increase to 13,845,779 as I manually constructed some more 6x6-9x9 cancellative magmas which settle a few more cases, but I'm probably in diminishing returns with this particular approach so won't try further).

[Terence Tao]

I'll update the README to reflect the new status and slightly improved statistics.

[Amir Livne Bar-on]

Shameless advertising - between the time I tested the Progress badge locally and when it was integrated in the main repo it grew from 86.9% to 87.6%. this is probably due to the additional counter-examples from larger magmas.

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

I made an attempt to naively port the transitive closure pruning script (generate_lean.py) to make it compatible with the cancellative 5x5s in this commit.

At first everything seemed to work, the proof goes through. However, inspecting the output of lake exe extract_implications outcomes --hist shows that we lose quite a few refutations!

Alas there are way too many places where things could go wrong, including in the original script, one of my changes, or even in the Lean code which counts/constructs the implicit refutations :( I won't have spare capacity to look into this any time soon, so I created Issue #265.

[Joachim Breitner]

I think I see the (or at least one) typo

    # prune by implications
    satisfied = set()
    for i in data["satisfied"]:
        # already implied
        if implying[i].intersection(satisfied):
          continue
        # remove all implied by this
        satisfied = satisfied - impliedBy[i]
        satisfied.add(i)
    refuted = set()
    for i in data["refuted"]:
        # already ruled out
        if impliedBy[i].intersection(refuted):
          continue
        # remove all that this is ruling out
        refuted = refuted - impliedBy[i]
        refuted.add(i)

The last impliedBy should be implying. I’ll make a PR fixing this in the existing code. Sorry for that.

[Joachim Breitner]

Hmm, I’m confused. It looks like on main the file equational_theories/Generated/All4x4Tables/Refutation0.lean contains a 2×2 magma, but the generate_lean.py script only handles 4×4 magmas. This came in @Zoltan A. Kocsis (Z.A.K.) ’s https://github.com/teorth/equational_theories/pull/224

I’m a bit confused by that PR. It seems that in that PR you are generating the lean files not with generate_lean.py, but something else, but left the python script in there? I’m also confused about the README, it mentions refutations.txt but that file does not exist anymore.

[Joachim Breitner]

Now it bites that we don’t have CI set up that checks that all generated lean files can be reproduced from the corresponding (calculated) data files :-/

[Joachim Breitner]

Fix in https://github.com/teorth/equational_theories/pull/271. The unknown count still goes up, so there might be another issue somewhere in the pipeline. But it’s still a worthwhile bug fix, so once someone had a look I think we should merge this.

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

Sorry if something's unclear @Joachim Breitner, indeed things have changed a bit with 224.

The Refutation*.lean files in the current main are generated using the generate_5x5_refutations.sh bash script from the file plan-5x5.txt (itself generated from other files by a heap of tools starting with Mace4, but it's not important: the plan-5x5.txt output is included in the distribution and needs no updates rn).

The bash script itself calls out to a Haskell tool, gen-refutations in finite_magma_tools which parses plan-5x5.txt and emits Lean.

However, gen-refutations does not read implications.json and does not do pruning - it's a throwaway tool, meant to eventually be replaced by an updated generate_lean.py which can handle something like plan-5x5.txt.I made an attempt at doing precisely that in the repo linked in that issue, but gave up since the implication counts didn't match.

Hope this makes more sense now.

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

I’m also confused about the README, it mentions refutations.txt but that file does not exist anymore.

NB refutations.txt did exist back when 224 was made, it was removed later on when #187 was merged.

[Joachim Breitner]

Ah, ok, so that PR is the one that would have broke the CI that I wish we had :-D. Sorry for the pointing fingers in the wrong direction.

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

No worries. I'll eliminate mentions of refutations.txt from both the readme and the bash script tomorrow.

[Joachim Breitner]

Zoltan A. Kocsis (Z.A.K.) said:

I made an attempt at doing precisely that in the repo linked in that issue, but gave up since the implication counts didn't match.

I’d say go ahead. The issue is already in the repo somewhere, and my https://github.com/teorth/equational_theories/pull/271 fixes at least part of the problem, so your change is not a regression. And with your update we have more uniformity in how we generate the lean files, so less moving parts to debug, and easier to fix when it’s fixed.

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

This is now PR #275, ready to merge.

@Joachim Breitner I didn't touch the generate_lean.py in Generated/FinSearch: there's currently a different hardcoded path in each of the two generate_lean.py files, and I didn't want to implement argument parsing as part of this PR (there is some urgency since it's techincally fixing a regression; we don't want people going on wild goose chases refuting stuff that's already known to be refuted).

[Daniel Weber]

I added more counterexamples at https://github.com/Command-Master/equational_theories/tree/VP-cex2/equational_theories/Generated/VampireProven, after giving it more time to run. How do I move them to All4x4Tables/data/vampire_generated.txt?

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

You can commit them as Disproofs.lean for now, and I'll move them tomorrow, along with other tables others asked for.

There's a PR coming, hoepfully tomorrow, which will make adding stuff to All4x4Tables much much easier, so there's not much point in me explaining the currenr process now.

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

The current process is:

1. putting them into vampire-generated.txt in the same format as the others there (this is not automated yet)
2. deleting plan.txt,
3. rerunning the shell script in src (this'll take 35mins or so to finish now), and then puthon3 generate_lean.py

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

But again, there's no point in learning this now, it's gonna be easy easy soon