New Andrews-Curtis trivializations for Miller-Schupp group presentations (Q6933180)

\textit{J. J. Andrews} and \textit{M. L. Curtis} [Proc. Am. Math. Soc. 16, 192--195 (1965; Zbl 0131.38301)] introduced a family of two-generator, two-relator groups was introduced in connection with topological problems on handle-bodies and contractible complexes in manifolds. The Andrews-Curtis conjecture, formulated in that context, remains open in general. However, in the particular case of the groups\N\[\NG(n) = \big \langle a, b \; \big | \; a^{-1} b^n a = b^{n+1},\ b^{-1} a b = a^2 \big \rangle,\N\]\Nit is known that \(G(n)\) is trivial for all \(n \in \mathbb{N}\), as proved in the work by \textit{C. F. Miller} and \textit{P. E. Schupp} [Contemp. Math. 250, 113--115 (1999; Zbl 0951.20022)].\N\NThe author revisits this question from a formal logic and rewriting perspective, demonstrating the triviality of \(G(n)\) for \(1 \leq n \leq 8\) through explicit derivations using a combination of Tietze transformations and automated reasoning via \texttt{Prover9}. Each case is carefully analyzed by deriving from the given relations the consequences \(a = b = 1\), under the sole assumptions of group axioms and the relators. The manipulations involve strategic conjugation and power identities, exploiting the commutativity of \(a\) with its powers.\N\NThe reviewer notes that the proof that \(G(n) = 1\) can be easily carried out by hand and that the derivation offers convincing support for Conjecture 2 proposed in the paper.