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.