Proof of Collatz Conjecture Using Division Sequence
- 1 Independent Scholar, Nankoku City, Japan
Abstract
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.
- Lagarias, J.C. (2010) The Ultimate Challenge: The 3x + 1 Problem. American Mathematical Society. https://doi.org/10.1090/mbk/078
- Tao, T. (2019) Almost All Orbits of the Collatz Map Attain Almost Bounded Values. https://arxiv.org/pdf/1909.03562.pdf
- Yolcu, E., Aaronson, S. and Heule, M.J.H. (2021) An Automated Approach to the Collatz Conjecture. In: Platzer, A. and Sutcliffe, G., Eds., Lecture Notes in Computer Science, Vol. 12699, Springer, Cham. https://doi.org/10.1007/978-3-030-79876-5_27
- Kamal, B. (2019) On the Probabilistic Proof of the Convergence of the Collatz Conjecture. Journal of Probability and Statistics, 2019, Article ID 6814378. https://doi.org/10.1155/2019/6814378
- Deloin, R. (2019) Proof of Collatz Conjecture. Asian Research Journal of Mathematics, 14, 1-18. https://doi.org/10.9734/arjom/2019/v14i230123
- Sultanow, E., Koch, C., and Cox, S. (2020) Collatz Sequences in the Light of Graph Theory. Universität Potsdam, Potsdam. https://doi.org/10.25932/publishup-44325
- Venkatesulu, M. and Devi Parameswari, C. (2019) Verification of Collatz Conjecture: An Algorithmic Approach Based on Binary Representation of Integers, https://arxiv.org/pdf/1912.05942.pdf
- Koch, C., Sultanow, E. and Cox, S. (2020) Divisions by Two in Collatz Sequences: A Data Science Approach. International Journal of Pure Mathematical Sciences, 21, 1-13. https://doi.org/10.18052/www.scipress.com/IJPMS.21.1
- Gonthier, G. (2005) A Computer-Checked Proof of the Four Colour Theorem. http://audentia-gestion.fr/MICROSOFT/4colproof.pdf
- Hales, T., Adams, M., Bauer, G., Tat Dat, D., Harrison, J., Le Truong, H., Kaliszyk, C., Magron, V., Mclaughlin, S., Thang, N.T., Truong, N.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Hoai An, T.T., Trung, T.N., Diep, T.T., Urban, J., Ky, V.K. and Zumkeller, R. (2015) A Formal Proof of the Kepler Conjecture. https://arxiv.org/pdf/1501.02155.pdf
- Kaliszyk, C., Urban, J., Michalewski, H. and Olšák, M. (2018) Reinforcement Learning of Theorem Proving. https://arxiv.org/pdf/1805.07563.pdf
- Huang, D., Dhariwal, P., Song, D. and Sutskever, I. (2018) GamePad: A Learning Environment for Theorem Proving. https://arxiv.org/pdf/1806.00608.pdf
- Minervini, P., Bosnjak, M., Rocktäschel, T. and Riedel, S. (2018) Towards Neural Theorem Proving at Scale. https://arxiv.org/pdf/1807.08204.pdf