An Automated Approach to the Collatz Conjecture

Explore an automated approach to the Collatz Conjecture in this 49-minute lecture by Emre Yolcu from Carnegie Mellon University. Delve into the theoretical foundations of SAT/SMT solving and automated deduction for mathematics. Learn about proving termination, matrix interpretations, and string rewriting techniques applied to the Collatz problem. Examine alternative rewriting systems, mixed binary-ternary representations, and nontrivial tests like Farkas' map. Investigate partial solutions and Collatz trajectories modulo 8. Gain insights into the challenges and potential of automated methods in tackling this famous mathematical conjecture.

Intro
Automated deduction for mathematics
Proving termination Baader and Nipkow, 1998
Matrix interpretations Hofbauer and Waldmann, 2006
Collatz conjecture
String rewriting for Collatz Zantema, 2005
Mixed binary-ternary representation
Alternative rewriting system for Collatz
Nontrivial test: Farkas' map [Farkas, 2005]
Partial solution
Collatz trajectories modulo 8
More problems
Closing remarks