All4x4Tables: Integrate straggler counterexamples

blueprint/src/chapter/counterexamples.tex

@@ -20,5 +20,7 @@ \chapter{Selected magmas}
   \item The set of strings with $x \circ y$ equal to $y$ when $x=y$ or when $x$ ends with $yyy$, or $xy$ otherwise (see \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/3102.20does.20not.20imply.203176}{this Zulip thread}).
   \item Vector spaces ${\mathbb F}_2^n$ over ${\mathbb F}_2$, which obey Definition \ref{eq1571} (and hence all the subsequent laws mentioned in Theorem \ref{1571_impl}).
   \item Knuth's construction \cite{knuth} of a central groupoid (Definition \ref{eq168}) as follows.  Let $S$ be a (finite) set with a distinguished element $0$, and a binary operation $*$ such that $x*0=0$ and $0*x=x$   for all $x$, and for each $x,y$ there is a unique $z$ with $x*z=y$.  One can then define a central groupoid on $S \times S$ by defining $(a,b) \op (c,d)$ to equal $(b,c)$ if $c,d \neq 0$; $(b,e)$ if $b*e=c$ is non-zero and $d=0$; and $(a*b,0)$ if $c=0$.  One such example in \cite{knuth} is when $S = \{0,1,2\}$ with $1*1=2*1=2$ and $1*2=2*2=1$.
-  \item A magma of cardinality $8$ was \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/using.20z3}{constructed by Z3} to refute an implication.
+  \item Cancellative magmas of orders 7 to 9, found by hand-guided search using various solvers.
+  \item Two magmas of cardinality $8$ were \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/using.20z3}{constructed by Z3}.
+  \item A large number of ad-hoc finite magmas were constructed using the Vampire theorem prover.
 \end{itemize}

equational_theories/Generated/All4x4Tables/README.md

@@ -3,14 +3,16 @@
 The Lean proofs here refute every false implication between two equations that
 has a counterexample in one of the following kinds of structures:
 
-* any `2x2`, `3x3` or `4x4` magma,
-* any cancellative `5x5` magma,
-* one of the 34 cancellative `7x7-9x9` magmas listed in `data/cancellative-manual.txt`.
+* every `2x2`, `3x3` or `4x4` magma,
+* every cancellative `5x5` magma,
+* a motley crew of other `5x5-9x9` finite magmas listed in `data/*.txt`.
 
-The proofs are generated by the following tools:
+Automated tools used to find these counterexamples include:
 
 1. The `2x2-4x4` magmas are brute-forced by a C program and pruned by Python scripts.
-2. The `5x5` magmas are generated using Mace4 and pruned using some Haskell tools.
+2. The `5x5` cancellative magmas are generated using Mace4 and pruned using some Haskell tools.
+3. Some magmas constructed by the Z3 solver, gathered from #308.
+4. A number of magmas constructed by the Vampire theorem prover, gathered from #276.
 
 # 2x2-4x4 magmas (brute-forcing)
 
@@ -50,23 +52,23 @@ and the script re-run to further reduce the size of the theorems.
 The brute-forcing takes a couple hundred CPU hours.
 
 
-# 5x5 cancellative magmas
+# 5x5 and above
 
 Once the 4x4 and smaller magmas have been brute-forced and `refutationsNxN.txt`
-generated, running the following bash scripts:
+generated, run the following bash scripts:
 ```
-MACE4HOME=/path/to/mace4 ./generate_5x5_refutations.sh
+MACE4HOME=/path/to/mace4 ./generate_combined_refutations.sh
 python3 generate_lean.py
 ```
 
 These scripts do the following:
 
 **1.** Use Mace4 to generate a list of all 5x5 cancellative magmas up to isomorphism.
 
-**2.** Take the `refutations.txt` obtained by enumerating 4x4 magmas, combines it with
-the 5x5 cancellative magmas and a hand-curated list of larger cancellative magmas,
-then uses the Haskell tools in `finite_magma_tools` to combine them into a shortlist
-of finite magma refutations which optimally cover the same set of counterexamples
+**2.** Take the `refutationsNxN.txt` files obtained by brute-forcing, combine it with
+the 5x5 cancellative magmas and a hand-curated list of other magmas, then use the
+Haskell tools in `finite_magma_tools` to combine them into a shortlist of finite
+magma refutations which optimally cover the same set of counterexamples
 as all of these. These proofs are output into the `raw_lean_output/` directory.
 
 **3.** Further prune the required `Fact`s using the known positive implications taken