Proof of Collatz Conjecture Using Division Sequence

The purpose of this study is to prove the Collatz conjecture using a theorem proving system. First, the division sequence is defined as an alignment of the number of times division by 2 is performed in the Collatz operation. Then, the star conversion is defined, which is a mapping from a specific division sequence to a division sequence. Here it is important to map to some division sequence, not which division sequence. The important point is that the finite length of the division sequence does not change before and after the star conversion. In theorem proving system, we considered two parallel methods: main-proof is a claim to a computer proposition that has the same meaning as the Collatz conjecture. Theorem proving support system “Idris” was used. Moreover, we sub-proved that the 12 “extended star conversion” are closed to the “Collatz operation”. Egison’s computer algebra system is used for proof. The results of the two methods achieved the goal of proving the Collatz conjecture using a theorem proving system.