677-255 (#1071)

Add 677-255 conjecture

paper/intro.tex

@@ -40,9 +40,7 @@ \subsection{The Equational Theories Project}
 
 \subsection{Outcomes}
 
-\note{This text assumes (optimistically) that both the original and finite implication graph will be completely formalized.}
-
-The ETP achieved its primary objectives, with all of the implications for both arbitrary magmas and finite magmas formalized in the proof assistant language \emph{Lean}, and can be found on the ETP GitHub repository.  See \Cref{fig:854}, \Cref{fig:1729} for some small fragments of the implication graphs produced. The experience of running such a large collaborative research project introduced several challenges, which we report upon in \Cref{project-sec}. Also, a variety of methods with varying degrees of automation or computer-assistance had to be developed to resolve all the implications, which had quite a variety of difficulty levels.
+The ETP achieved almost all of its primary objectives, with almost all of the implications for both arbitrary magmas and finite magmas formalized in the proof assistant language \emph{Lean}, and can be found on the ETP GitHub repository.  See \Cref{fig:854}, \Cref{fig:1729} for some small fragments of the implication graphs produced.  While the implication graph for the arbitrary magma entailment relation $\vdash$ was completely determined and formalized, one of the $22033636$ implications (and its dual) for the finite magma entailment relation $\vdashfin$ remains open.  Specifically, we were unable to obtain either a human-readable or formalized proof or disproof of the implication $E677 \vdashfin E255$ (or its equivalent dual $E2910 \vdashfin E47$), despite extensive efforts from the participants of the project; we tentatively conjecture this implication to be false (i.e., that there exists a finite magma obeying \eqref{eq677} but not \eqref{eq255}), but the refutation appears to be ``immune'' to most of the techniques that we developed for the project.  (We were however able to establish that the corresponding implication $E677 \vdash E255$ for arbitrary magmas was false, using the greedy construction discussed in \Cref{greedy-sec}.)
 
 \begin{figure}
 \centering

paper/main.tdo

@@ -1,3 +1,3 @@
 \contentsline {todo}{Shreyas Srinivas and Pietro Monticone have volunteered to take the lead on this section.}{10}{section*.2}%
-\contentsline {todo}{Discuss how the above breaks down when a large and diverse collection of collaborators work over the internet. Consider citing the \href {https://euromathsoc.org/code-of-practice}{EMS webpage for code of practice} for joint responsibility rules }{10}{section*.3}%
-\contentsline {todo}{elaborate on what level of overlap was permissible and what we consider excessive}{12}{section*.4}%
+\contentsline {todo}{Discuss how the above breaks down when a large and diverse collection of collaborators work over the internet. Consider citing the \href {https://euromathsoc.org/code-of-practice}{EMS webpage for code of practice} for joint responsibility rules }{11}{section*.3}%
+\contentsline {todo}{elaborate on what level of overlap was permissible and what we consider excessive}{13}{section*.4}%

paper/numbering.tex

@@ -46,40 +46,44 @@ \section{Numbering system}\label{numbering-app}
 
 Below we record some specific equations appearing in this paper, using the alphabet $\x,\y,\z,\w,\uu,\vv$ in place of $0,1,2,3,4,5,\dots$ for readability.
 \begin{align}
-        \x &\formaleq \x & \hbox{(Trivial law)} \label{eq1}\tag{E1} \\
-        \x &\formaleq \y & \hbox{(Singleton law)} \label{eq2}\tag{E2} \\
-        \x &\formaleq \x \op \x & \hbox{(Idempotent law)} \label{eq3}\tag{E3} \\
-        \x &\formaleq \x \op \y & \hbox{(Left-absorptive law)} \label{eq4}\tag{E4} \\
-        \x &\formaleq \y \op \x & \hbox{(Right-absorptive law)} \label{eq5}\tag{E5} \\
-        \x &\formaleq \x \op (\y \op \x) \label{eq10}\tag{E10} \\
-        \x &\formaleq (\x \op \x) \op \x \label{eq23}\tag{E23} \\
-        \x \op \x &\formaleq \y \op \z \label{eq41}\tag{E41} \\
-        \x \op \y &\formaleq \y \op \x & \hbox{(Commutative law)} \label{eq43}\tag{E43} \\
-        \x \op \y &\formaleq \z \op \w & \hbox{(Constant law)} \label{eq46}\tag{E46} \\
-        \x &\formaleq \y \op (\y \op (\x \op \y))  \label{eq73}\tag{E73} \\
-        \x &\formaleq (\x \op \x) \op (\x \op \x) \label{eq151}\tag{E151} \\
-        \x &\formaleq (\y \op \x) \op (\x \op \z) & \hbox{(Central groupoid law)} \label{eq168}\tag{E168} \\
-        \x &\formaleq (\x \op (\x \op \y)) \op \y \label{eq206}\tag{E206} \\
-        \x \op \y &\formaleq \x \op (\y \op \z) \label{eq327}\tag{E327} \\
-        \x &\formaleq (\x \op \y) \op \y \label{eq378}\tag{E378} \\
-        \x \op \y &\formaleq (\z \op \x) \op \y \label{eq395}\tag{E395} \\
-        \x &\formaleq \y \op ( (\z \op (\x \op (\y \op \z)))) & \hbox{(Tarski's axiom)} \label{eq543}\tag{E543} \\
-        \x &\formaleq \x \op ((\y \op \z) \op (\x \op \z)) \label{eq854}\tag{E854}\\
-        \x &\formaleq \y \op ((\y \op (\x \op \x)) \op \y) \label{eq1110}\tag{E1110} \\
-        \x &\formaleq \y \op ((\y \op (\x \op \z)) \op \z) \label{eq1117}\tag{E1117} \\
-        \x &\formaleq \y \op (((\x \op \y) \op \x) \op \y) \label{eq1286}\tag{E1286} \\
-        \x &\formaleq (\y \op \x) \op (\x \op (\z \op \y)) & \hbox{(Weak central groupoids)}\label{eq1485}\tag{E1485} \\
-        \x &\formaleq (\y \op \z) \op (\y \op (\x \op \z)) & \hbox{(Exp. $2$ abelian groups)} \label{eq1571}\tag{E1571} \\
-        \x &\formaleq (\x \op \x) \op ((\x \op \x) \op \x) \label{eq1629}\tag{E1629} \\
-        \x &\formaleq (\x \op \y) \op ((\x \op \y) \op \y) \label{eq1648}\tag{E1648} \\
-        \x &\formaleq (\x \op \y) \op ((\y \op \y) \op \z) \label{eq1659}\tag{E1659} \\
-        \x &\formaleq (\y \op \x) \op ((\x \op \z) \op \z) \label{eq1689}\tag{E1689} \\
-        \x &\formaleq (\y \op \y) \op ((\y \op \x) \op \y) \label{eq1729}\tag{E1729} \\
-        \x &\formaleq (\y \op (\x \op (\y \op x))) \op y \label{eq2301}\tag{E2301} \\
-        \x &\formaleq (\x \op ((\x \op \x) \op \x)) \op \x \label{eq2441}\tag{E2441} \\
-        \x \op \y &\formaleq \x \op (\y \op (\x \op \y)) \label{eq3316}\tag{E3316}
-    \end{align}
+    \x &\formaleq \x & \hbox{(Trivial law)} \label{eq1}\tag{E1} \\
+    \x &\formaleq \y & \hbox{(Singleton law)} \label{eq2}\tag{E2} \\
+    \x &\formaleq \x \op \x & \hbox{(Idempotent law)} \label{eq3}\tag{E3} \\
+    \x &\formaleq \x \op \y & \hbox{(Left-absorptive law)} \label{eq4}\tag{E4} \\
+    \x &\formaleq \y \op \x & \hbox{(Right-absorptive law)} \label{eq5}\tag{E5} \\
+    \x &\formaleq \x \op (\y \op \x) \label{eq10}\tag{E10} \\
+    \x &\formaleq (\x \op \x) \op \x \label{eq23}\tag{E23} \\
+    \x \op \x &\formaleq \y \op \z \label{eq41}\tag{E41} \\
+    \x \op \y &\formaleq \y \op \x & \hbox{(Commutative law)} \label{eq43}\tag{E43} \\
+    \x \op \y &\formaleq \z \op \w & \hbox{(Constant law)} \label{eq46}\tag{E46} \\
+    \x &\formaleq \x \op (\x \op (\x \op \x)) \label{eq47}\tag{E47} \\
+    \x &\formaleq \y \op (\y \op (\x \op \y))  \label{eq73}\tag{E73} \\
+    \x &\formaleq (\x \op \x) \op (\x \op \x) \label{eq151}\tag{E151} \\
+    \x &\formaleq (\y \op \x) \op (\x \op \z) & \hbox{(Central groupoid law)} \label{eq168}\tag{E168} \\
+    \x &\formaleq (\x \op (\x \op \y)) \op \y \label{eq206}\tag{E206} \\
+    \x &\formaleq ((\x \op \x) \op \x) \op \x \label{eq255}\tag{E255} \\
+    \x \op \y &\formaleq \x \op (\y \op \z) \label{eq327}\tag{E327} \\
+    \x &\formaleq (\x \op \y) \op \y \label{eq378}\tag{E378} \\
+    \x \op \y &\formaleq (\z \op \x) \op \y \label{eq395}\tag{E395} \\
+    \x &\formaleq \y \op ( (\z \op (\x \op (\y \op \z)))) & \hbox{(Tarski's axiom)} \label{eq543}\tag{E543} \\
+    \x &\formaleq \y \op (\x \op ((\y \op \x) \op \y)) \label{eq677}\tag{E677} \\
+    \x &\formaleq \x \op ((\y \op \z) \op (\x \op \z)) \label{eq854}\tag{E854}\\
+    \x &\formaleq \y \op ((\y \op (\x \op \x)) \op \y) \label{eq1110}\tag{E1110} \\
+    \x &\formaleq \y \op ((\y \op (\x \op \z)) \op \z) \label{eq1117}\tag{E1117} \\
+    \x &\formaleq \y \op (((\x \op \y) \op \x) \op \y) \label{eq1286}\tag{E1286} \\
+    \x &\formaleq (\y \op \x) \op (\x \op (\z \op \y)) & \hbox{(Weak central groupoids)}\label{eq1485}\tag{E1485} \\
+    \x &\formaleq (\y \op \z) \op (\y \op (\x \op \z)) & \hbox{(Exp. $2$ abelian groups)} \label{eq1571}\tag{E1571} \\
+    \x &\formaleq (\x \op \x) \op ((\x \op \x) \op \x) \label{eq1629}\tag{E1629} \\
+    \x &\formaleq (\x \op \y) \op ((\x \op \y) \op \y) \label{eq1648}\tag{E1648} \\
+    \x &\formaleq (\x \op \y) \op ((\y \op \y) \op \z) \label{eq1659}\tag{E1659} \\
+    \x &\formaleq (\y \op \x) \op ((\x \op \z) \op \z) \label{eq1689}\tag{E1689} \\
+    \x &\formaleq (\y \op \y) \op ((\y \op \x) \op \y) \label{eq1729}\tag{E1729} \\
+    \x &\formaleq (\y \op (\x \op (\y \op x))) \op \y \label{eq2301}\tag{E2301}
+\end{align}
     \begin{align}
+        \x &\formaleq (\x \op ((\x \op \x) \op \x)) \op \x \label{eq2441}\tag{E2441} \\
+        \x &\formaleq ((\y \op (\x \op \y)) \op \x) \op \y \label{eq2910}\tag{E2910} \\
+        \x \op \y &\formaleq \x \op (\y \op (\x \op \y)) \label{eq3316}\tag{E3316} \\
         \x \op (\y \op \x) &\formaleq \x \op (\y \op \z) \label{eq4315}\tag{E4315} \\
         \x \op (\x \op \x) &\formaleq (\x \op \x) \op \x \label{eq4380}\tag{E4380} \\
         \x \op (\y \op \y) &= (\y \op \y) \op \x \label{eq4482}\tag{E4482} \\