All4x4Tables: update after #281 #294
Conversation
The script at `equational_theories/Generated/All4x4Tables/src/generate_lean.py` is supposed to read the implications.json file, and prune the finite magma checks based on that, so that we don't have to generate redundant explicit refutations that already follow from the known implications. I recently ported this script to work with the cancellative magmas added in teorth#224. Unfortunately, there seems to be a bug in this naive port: once we move to implicit refutations, the total proof_false decreases, and the number of unknowns increases. For example, running on a now-recent main we have ``` BEFORE (explicit proofs in All4x4Tables): {"explicit_proof_true": 28263, "implicit_proof_true": 5457962, "unknown": 2726304, "implicit_proof_false": 3486, "explicit_proof_false": 13845794 } AFTER (implicit proofs in All4x4Tables): {"explicit_proof_true": 28263, "implicit_proof_true": 5457962, "unknown": 2744422, "implicit_proof_false": 13185894, "explicit_proof_false": 645268 } ``` To reproduce, 1. Generate an `implications.json` using `lake exe extract_implications --json --only-implications equational_theories` 2. Run the version of `generate_lean.py` from this commit. 3. Build the proofs, then inspect the output of `lake exe extract_implications outcomes --hist`.
Adds `make-plan` output format support to `generate_lean.py` so that it can
be used to prune the refutation set of the cancellative 5x5 magmas using the
already proven implications read from `implications.json`.
Of the previous 196990 facts that we had to check explicitly, pruning removed
172724 facts, leaving 24266 facts to check (a 87% improvement).
The count of unknowns is unaffected, as `extract_implications outcomes --hist`
confirms:
```
{"explicit_proof_true": 28264,
"implicit_proof_true": 5457961,
"unknown": 2726304,
"implicit_proof_false": 13243426,
"explicit_proof_false": 605854
}
```
Adds 4 more cancellative magmas that were found through hand-guided
search and which refute 31 still-open implications. These were still
open following the vampire theorems.
The magmas were found by hand-searching for cancellative magmas that
fail to satisfy large one-variable laws.
As an added benefit, the number of explicit false proofs is reduced
by a further 1.1k.
{"explicit_proof_true": 28264,
"implicit_proof_true": 5457961,
"unknown": 2726273,
"implicit_proof_false": 13244610,
"explicit_proof_false": 604701
}
Since the Vampire proofs (teorth#281) are merged, we re-run the transitive closure pruning using the larger implication set. This further reduces the number of explicit checks that we have to perform. The number of unknown implications is reduced from 29688 to 29657
I'll probably get around to building something more user-friendly for this in the near future, but the current situation is this:
[Here] is an example of such an input file, but as you can see it already has to contain an exact list of equations satisfied in a given magma. (FinSearch has something similar - the two dirs will eventually be merged, but we'll have to sort out how this goes). The |
|
Ultimately one could imagine a web interface where one could upload (in some standard format) a multiplication table, the tool displays all the equations it satisfies, checks if it creates any new refutations, and if so it accepts the table and adds it to some standard directory from which the refutations are generated. There may be a few thousand finite magma refutations left out there, so this might be worthwhile. Anyway, I made a link here from #180 which one can re-interpret as asking for this sort of user-friendly functionality. |
This PR:
1. Adds 4 more cancellative magmas that were found through hand-guided search and which refute 31 of the 29688 implications still open after #281, bringing down the number to 29657. The idea was to find for cancellative magmas that specifically fail to satisfy large one-variable laws. The addition of the new magmas also results in a slightly better plan (with fewer Lean checks required).
2. Re-runs the transitive closure pruning using the large number of recently proved implications. This further pushes down the number of explicitly proven implications from 604701 to 581162 .
3. Adds a minor QoL improvement to variable counting in
finite_magma_tools, which makes it more useful for #278 -style experimentation.