An Automated Approach to the Collatz Conjecture

TL;DR

This paper introduces a novel string rewriting system to analyze the Collatz conjecture, establishing an equivalence between the conjecture and termination of this system, and demonstrates partial automated proofs using matrix interpretations.

Contribution

It presents a new rewriting system modeling the Collatz conjecture and explores automated proof techniques, offering a fresh approach to this longstanding problem.

Findings

Rewriting system simulates Collatz iterations on mixed binary-ternary strings.

Termination of the system is equivalent to the Collatz conjecture.

Automated proofs of weakened conjectures are achieved using matrix interpretations.

Abstract

We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary-ternary representations of positive integers. We prove that the termination of this rewriting system is equivalent to the Collatz conjecture. We also prove that a previously studied rewriting system that simulates the Collatz function using unary representations does not admit termination proofs via natural matrix interpretations, even when used in conjunction with dependency pairs. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses natural/arctic matrix interpretations and we find automated proofs of nontrivial weakenings of the Collatz conjecture. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach.