Abstract
In this talk, I will present our exploration of the Collatz conjecture and its generalized variants through the lens of termination of string rewriting. I will describe a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary-ternary representations of positive integers. Termination of this rewriting system is a question equivalent to the Collatz conjecture, which makes it possible to search for a proof of the Collatz conjecture via the automated methods used for proving termination (e.g., matrix/arctic interpretations). To exhibit the feasibility of this approach in proving mathematically interesting statements, I will show that it succeeds for some nontrivial weakenings of the Collatz conjecture. This is joint work with Scott Aaronson and Marijn Heule.