Semigroup Identities, Proofs, and Artificial Intelligence

It is known that if every group satisfying an identity of the form yx ~ xU(x,y)y is abelian, so is every semigroup that satisfies that identity. Because a group has an identity element and the cancellation property, it is easier to show that a group is abelian than that a semigroup is. If we know that it is, then there must be a sequence of substitutions using xU(x,y)y ~ yx that transforms xy to yx. We examine such sequences and propose finding them as a challenge to proof by computer. Also, every model of y ~ xU(x,y)x is a group. This raises a similar challenge, which we explore in the special case y ~ x^my^px^n. In addition we determine the free model with two generators of some of these identities. In particular, we find that the free model for y ~ x^2yx^2 has order 32 and is the product of D4 (the symmetries of a square), C2, and C2, and point out relations between such identities and Burnside's Problem concerning models of x^n= e.