Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

All4x4Tables: update after #281 #294

Merged
merged 4 commits into from
Oct 5, 2024
Merged

All4x4Tables: update after #281 #294

merged 4 commits into from
Oct 5, 2024

Commits on Oct 5, 2024

  1. All4x4Tables: BUG lost implications after pruning 

    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`.
    @zaklogician
    zaklogician committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    88446f9 View commit details
    Browse the repository at this point in the history

  2. All4x4Tables: pruning for cancellative 5x5 magmas (teorth#264) 

    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
}
```
    @zaklogician
    zaklogician committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    4a9dd7f View commit details
    Browse the repository at this point in the history

  3. All4x4Tables: more hand-curated cancellative magmas 

    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
}
    @zaklogician
    zaklogician committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    9ad7189 View commit details
    Browse the repository at this point in the history

  4. All4x4Tables: update transitive closure pruning for teorth#281 

    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
    @zaklogician
    zaklogician committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    b8f3406 View commit details
    Browse the repository at this point in the history