Add refutations for entries of most_wanted.md found by searching for small magmas

[few]

This adds a number of refutations for entries in most_wanted.md found by searching for magmas over Fin N, with N=2..5.
The Lean proofs are generated by a Python script and use (several versions of) a template I came up with. Note that these were my first steps with Lean and certainly not ideal.

Also note that for some other entries, there are already proofs in other files of this repository.

[carlini]

Could you please follow the other steps here https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md#automated-proofs, including adding your python source and a brief explanation of how these were generated?

[few]

Sorry for missing that. I have updated the branch accordingly.

[nomeata]

Is this subsumed by #111?

[nomeata]

Also, it’s not really efficient to prove and state each antiimplication separately. See https://github.com/teorth/equational_theories/blob/main/equational_theories/SmallMagmas.lean how to express all facts about a single magma in one theorem. And likely the decideFin! tactic used there helps in your case too!

[few]

Is this subsumed by #111?

Partially. Basically all theorems involving Fin 2, Fin 3 and Fin 4 should be redundant. But finsearch.py can go beyond 4 as can be seen by the theorems involving Fin 6. There should be no counter example with a smaller magma.

[few]

Also, it’s not really efficient to prove and state each antiimplication separately. See https://github.com/teorth/equational_theories/blob/main/equational_theories/SmallMagmas.lean how to express all facts about a single magma in one theorem. And likely the decideFin! tactic used there helps in your case too!

Thank you for the pointers, I'll see if I can make some progress on my own later.

[nomeata]

But finsearch.py can go beyond 4 as can be seen by the theorems involving Fin 6.

Good point. It would be good to see if they actually find new anti-implications that way, though.

[few]

I have updated the branch to only include theorems for equations that involve Fin 5. The theorems now use the same technique as SmallMagma.lean.

Modulo bugs in the program, the equations with theorems have no smaller magma that satisfies them. And there are no other equations that could be satisfied by a Fin 5 magma.
What is incomplete are the counterexamples, i.e., there are other Fin 5 magmas that refute some implications currently missing in the theorems.

Is there some easy way to check if any of the refutations in the theorems are already present somewhere else? Do we have a list of all known (non)implications?

[nomeata]

I think it would be wise to split the script into two steps

• one that does the search, and generates a list of interesting magmas and the equations it satisfies, and dumps that into a text file

• one that takes that and produces the lean files.

The reasons are

• we may need to adjust the syntax of theorems, and that should not require running slow scripts, nor random scripts.
• that second script should reduce the equations actually mentioned in the proof, like in https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/All4x4Tables/src/generate_lean.py, based on known implications. We should definitely do that here too, it reduces the size of these proofs considerably.

In fact, if your script produces data in the same format, you can just use the same script.

In fact in fact, and maybe not yet in this PR, we’ll converge on a single data format for facts about small magmas, and convert them to Lean in one go, which will avoid duplication and help with pruning.

[nomeata]

Suggested change

	equational_theories/Generated/FinSearch/theorems/FinSearch.lean linguist-generated
	equational_theories/Generated/FinSearch/theorems/magmas*.lean linguist-generated
	equational_theories/Generated/FinSearch/theorems/proofs*.lean linguist-generated
	equational_theories/Generated/FinSearch/FinSearch.lean linguist-generated

[nomeata]

Is there some easy way to check if any of the refutations in the theorems are already present somewhere else? Do we have a list of all known (non)implications?

You can run lake exe extract_implications. But as mentioned above I suggest you produce your data as non-lean files first, and then convert to lean using essentially the same script that I linked above; this will prune the facts based on known implications and on non-implications from the same file.

[few]

Thanks for the feedback. I have updated the PR as requested.

I have copied generate_lean.py from All4x4Tables as I needed to make some modifications.

[nomeata]

LGTM

[few]

Anything that needs to happen for this to be merged?

[nomeata]

Sorry, maybe I should have just pressed the button. There is a small merge conflict now, though.

[few]

Sorry, maybe I should have just pressed the button. There is a small merge conflict now, though.

Fixed