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

TL;DR

This paper revisits the stable Andrews-Curtis trivialization of the AK(3) presentation of the trivial group, providing an alternative proof via automated deduction and proposing computational challenges for future research.

Contribution

It introduces an automated deduction approach to prove stable AC-equivalence of AK(3), offering new transformation sequences and encouraging computational search methods.

Findings

Automated deduction successfully certifies stable AC-equivalence.

Multiple transformation sequences derived from automated proofs.

Proposes computational challenges for searching stable AC-transformations.

Abstract

Recent work by Shehper et al. (2024) demonstrated that the well-known Akbulut-Kirby AK(3) balanced presentation of the trivial group is stably AC-equivalent to the trivial presentation. This result eliminates AK(3) as a potential counterexample to the stable Andrews-Curtis conjecture. In this paper, we present an alternative proof of this result using an automated deduction approach. We provide several transformation sequences, derived from two different proofs generated by the automated theorem prover Prover9, that certify the stable AC-equivalence of AK(3) and the trivial presentation. We conclude by proposing a challenge to develop computational methods for searching stable AC-transformations.