E677 implies E255 for finite magmas

Open

FiniteMagmaE677.e677_implies_e255_finite

by mysticflounder · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

e255e677equational-theoriesfinite-magma

Open conjecture. For every finite type $A$ and arbitrary total operation $\diamond:A\times A\to A$ , E677 implies E255:

\left(\forall x,y\in A,\quad x=y\diamond\bigl(x\diamond((y\diamond x)\diamond y)\bigr)\right)\Longrightarrow\left(\forall x\in A,\quad x=((x\diamond x)\diamond x)\diamond x\right).

Empty finite carriers are included and make both universal statements vacuous.

Preamble

import Definitions.Def_FiniteMagmaE677

universe u

Formal statement

theorem FiniteMagmaE677.e677_implies_e255_finite {α : Type u} [Fintype α]
    (op : α → α → α) (h : FiniteMagmaE677.E677 op) : FiniteMagmaE677.E255 op := by sorry

Source

Matthew Bolan et al., The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale, arXiv:2512.07087v2 (December 16, 2025), Section 8, Problem 8.1, https://arxiv.org/html/2512.07087v2

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For every universe u, finite possibly empty type $\alpha:\mathrm{Type}\,u$ , and arbitrary binary operation $\operatorname{op}:\alpha\to\alpha\to\alpha$ , if every $a,b\in\alpha$ satisfy $a=\operatorname{op}\bigl(b,\operatorname{op}(a,\operatorname{op}(\operatorname{op}(b,a),b))\bigr)$ , then every $x\in\alpha$ satisfies $x=\operatorname{op}\bigl(\operatorname{op}(\operatorname{op}(x,x),x),x\bigr)$ ; for an empty $\alpha$ , both the hypothesis and conclusion are universal propositions holding vacuously.

View graph