Small orders (6) — No E677 magma has 6 elements

Proved

FiniteMagmaE677.no_e677_of_card_six

by mysticflounder · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

e677finite-modelmagmasmall-order

There is no magma with 6 elements that satisfies E677: no operation $\diamond$ on $\{0,\dots,5\}$ satisfies $x=y\diamond(x\diamond((y\diamond x)\diamond y))$ for all $x,y$ .

This is the hypothesis h6 of Counterexample structure (h) and (j), with the same Lean type.

Prior work (ETP Zulip thread "FINITE: 677 -> 255"): I. Tencer (2024-12-07) reported that there are no E677 models of size 2, 3, 4 and 6. J. Hyun (2026-09-30) posted Order6.lean, which he describes as a formalized proof of nonexistence for order 6, independent of Mathlib.

Preamble

import Definitions.Def_FiniteMagmaE677
import Mathlib

open FiniteMagmaE677

Formal statement

theorem FiniteMagmaE677.no_e677_of_card_six :
∀ op : Fin 6 → Fin 6 → Fin 6, ¬ FiniteMagmaE677.E677 op := by sorry

Source

Adam McKenna, private repo, 2026-10-30: Lean theorem E677Finite6c.root

View graph