Single axioms for groups (Q688567)

This paper demonstrates the difference of approach to proving certain mathematical facts by an oldfashioned mathematician [like the reviewer] and a mathematician versed in theorem proving by computers, and it illustrates the strength of the latter approach. The reviewer had found various single axioms that define the variety of groups in terms of a binary operation, namely multiplication or multiplication of inverses, and a unary operation, namely inversion [\textit{B. H. Neumann}, Bull. Aust. Math. Soc. 23, 81-102 (1981; Zbl 0581.20003), Ill. J. Math. 30, 295-300 (1986; Zbl 0581.20004)=Selected works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1076- 1097, 1098-1103]. The laws were of the form \(u=v\), where \(v\) had length 1 and \(u\) had length 18 and involved 4 variables; and the reviewer conjectured that these numbers could not be reduced. The author disproves these conjectures by exhibiting laws with \(u\) of length 18 in only 3 variables and with \(u\) of length 16 in 4 variables. These laws were found by the author and by \textit{W. W. McCune} [see the following review Zbl 0794.20002] using the automated theorem-proving program OTTER. The author first proves explicitly some known results, which were stated, without proof [``not very difficult to prove \dots We omit the proofs''] by \textit{G. Higman} and \textit{B. H. Neumann} [Publ. Math. 2, 215-221 (1953; Zbl 0050.25303) = Selected works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1069-1075]. For example, to prove the known result that at least 3 variables are needed in the laws, the author exhibits an elegant Moufang loop of order 10, which is, moreover, boolean: this, apparently the smallest properly non-associative di-associative loop, was also found using a computer program. The computer was also extensively used to prove other results contained in the literature, for example that at least three inversions must occur. The author exhibits 8 laws of the above form, in 3 variables, with \(u\) in 4 of them of length 18 and in 4 of length 20; some obvious transformations quadruple the laws to 32. The difference in lengths stems from the fact that the first 4 laws contain 5 inversions in \(u\), the last 4 contains 7. The author conjectures that fewer than 5 inversions will not suffice, and states some more unsolved problems. \{The reviewer found the notation difficult to follow, because it is traditional functional notation, which requires numerous separators, namely commas and parentheses\}.