{"id":"palomar/PALOMAR-2026-09-30-000005","url":"https://github.com/carlok/magma-1518-obstruction-lean/tree/eb2bbde8c137570d0e281a237187f5323a1b0a2d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000005-v1.json","repo":"https://github.com/carlok/magma-1518-obstruction-lean","tags":["math.RA","math.LO","msc:20N02","msc:08B05","msc:03C05","msc:68V20","lean","universal-algebra","magmas","equational-theories"],"score":0,"title":"One-generated (1518 + 3862)-magmas are trivial or the Z/3 shift; an explicit family of finite 1518-magmas violating laws 47, 614, 817, 3862","trust":"high","domain":"math.RA","source":"palomar","authors":["Carlo Perassi"],"reviews":0,"subject":"math.RA","summary":"Lean 4 results (core Lean, no dependencies, no axioms beyond the standard three) about law 1518 of the Equational Theories Project, x = (y ◇ y) ◇ (x ◇ (y ◇ x)). Theorem A: in every magma satisfying 1518 and 3862 (x ◇ x = (x ◇ (x ◇ x)) ◇ x), writing S x = x ◇ x, the set {x, S x, S (S x)} is closed under ◇ with u ◇ v = S v and S (S (S x)) = x; hence every one-generated such magma is the trivial magma or the three-element cyclic shift x ◇ y = y + 1. This proves a classification conjectured by Terence Tao on the Lean Zulip on 2024-11-29 (message 485148288). That message assumed 1518 together…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true}