New Andrews–Curtis trivializations for Miller–Schupp group presentations

We present recent developments in the applications of automated theorem proving in the investigation of the Andrews–Curtis conjecture. We demonstrate previously unknown trivializations of group presentations from a parametric family M S n ( w ∗ ) of trivial group presentations for n = 3 , 4 , 5 , 6 , 7 , 8 (subset of well-known Miller–Schupp family). Based on the human analysis of these trivializations we formulate two conjectures on the structure of simplifications for the infinite family M S n ( w ∗ ) , n ≥ 3 . • New examples of Andrews–Curtis trivilaizations are demonstrated. • Two conjectures on structural properties of trivializations sequences are presented. • The strength of generic automated reasoning methods in group theory is demonstrated.