Transitive closure pruning the finite magmas #265
Comments
This was referenced Oct 4, 2024
teorth
pushed a commit
that referenced
this issue
Oct 4, 2024
I implemented `make-plan` output format support in `generate_lean.py`. This means that it can now be used to prune the refutation set of the cancellative 5x5 magmas using the already proven implications read from `implications.json`. This greatly reduces the number of explicit proofs we have to do: of the previous 196990 facts that we had to check explicitly, pruning leaves only 24266 (a 87% improvement). Since #271 fixed the bug that led to lost implications, this now put us back on 2726304 unknowns. Merging this will resolve issue #265 . --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
|
Is this task now completed, or should the issue remain open? |
|
This was resolved by #275 . |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In
equation_theories/Generated/All4x4Tables, we refute potential implications between equational laws by finding small finite counterexamples. These counterexamples are generated by automated tools.Originally, the generated counterexamples were pruned using the graph of known implications (#196).
The recent addition of 5x5 cancellative magmas broke this pruning process (#224): the file format changed substantially, and the existing pruning script (
All4x4Tables/src/generate_lean.py) cannot handle it.Making the pruning work again could substantially speed up the checking of
All4x4Tables, and further cut down on the number of magmas we need. This could be done by fixing the existing pruning script, or writing a new one (but see the note below regarding the former).Note:
I made an attempt to naively port the script to make it compatible with the changed file format here. At first everything seemed to work, the proof goes through. However, inspecting the output of
lake exe extract_implications outcomes --histshows that we lose quite a few refutations! Unfortunately, there are many places where things could go wrong, including in the original script, one of my changes, or even in the Lean code which counts implicit proofs. As of now I have no spare capacity to look into this myself, but am happy to assist if somebody takes it up.The text was updated successfully, but these errors were encountered: