Teaching the Computer how to Discover(!) and then Prove(!!) (all by Itself(!!!)) Analogs of Collatz's Notorious 3x+1 Conjecture

TL;DR

This paper presents a computer program that learns to discover and prove analogs of the Collatz conjecture using symbolic reasoning, successfully reproducing known results and generating new theorems autonomously.

Contribution

It introduces a novel automated theorem proving approach that leverages human ideas to discover and prove mathematical analogs, advancing computer-assisted mathematical discovery.

Findings

Reproduced ten known theorems using the program

Generated 134 new theorems with proofs autonomously

Demonstrated potential for solving the original Collatz conjecture

Abstract

Paul Erdos claimed that mathematics is not yet ready to settle the 3x+1 conjecture. I agree, but very soon it will be! With the exponential growth of computer-generated mathematics, we (or rather our silicon brethrern) would have a shot at it. Of course, not by number crunching, but by symbol crunching and automatic deduction. In the present article, I taught my computer how to use the brilliant ideas of four human beings (Amal Amleh, Ed Grove, Candy Kent, and Gerry Ladas) to prove two-dimensional analogs of this notorious conjecture. Once programmed (using my Maple package LADAS) it reproduced their ten theorems, and generated 134 new ones, complete with proofs. All by itself! I believe that the proof of the original 3x+1 conjecture would be in the same vein, but one would need a couple of extra human ideas, and better computers.