Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction

Recent work by Shehper et al. (2024) [13] proposed that the well-known Akbulut–Kirby presentation AK ( 3 ) is stably Andrews–Curtis (AC) equivalent to the trivial presentation, based on a reduction to a previously studied presentation P . In this paper, we present an independently obtained reduction of AK ( 3 ) to P , using a fully automated theorem proving approach. Subsequent to our initial submission, it has emerged that the earlier theoretical claim about the stable AC-trivializability of P —on which the Shehper et al. result relied—was based on an incorrect theorem, and thus the status of AK ( 3 ) remains unresolved. While this paper does not establish the stable AC-triviality of AK ( 3 ) , it contributes a reproducible and verifiable case study in the use of automated reasoning to analyze deep problems in combinatorial group theory. We conclude by suggesting future directions for computational exploration of stable AC-transformations.