Stable Andrews-Curtis trivialization of AK(3) revisited. A case study using automated deduction
Alexei Lisitsa
TL;DR
The paper addresses whether $AK(3)$ is stably AC-trivializable and achieves this via automated deduction by encoding AC-transformations into a first-order implicational framework. Using Prover9, it produces multiple transformation sequences connecting a presentation $P$ to $AK(3)$ and back, including sequences of lengths $252$, $160$, $70$, and $57$ from one approach and $110$ from a variant, thereby certifying stable AC-equivalence. It also contrasts these results with a recent greedy search that found a shorter sequence, highlighting the impact of rule-sets and encoding on the search for AC-simplifications. The work demonstrates that generic theorem-proving techniques can yield concrete AC-trivializations for challenging presentations and underscores the need for computational methods to target 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.