Goal

The goal of the Collatz Conjecture Challenge (ccchallenge for short) is to collaboratively formalise the research literature on the Collatz conjecture using proof assistants.

The Collatz Conjecture

The Collatz problem is known under many names such as: the \(3n + 1\) problem, the \(3x + 1\) problem, Ulam's conjecture, Thwaites' conjecture, the Syracuse problem, etc. The essence of the problem seems to trace back to Lothar Collatz's notebooks from the 1930s and is known to have circulated in mathematical circles in the 1950s [Lagarias, 2021]. The first printed occurrence of the problem seems to be a 1971 written version of a lecture by H. S. Coxeter [Coxeter, 1971].

Let \(\mathbb{N} = \{0, 1, 2, \ldots\}\) be the set of natural numbers and \(\mathbb{N}^+ = \{1, 2, \ldots\}\). The Collatz process is defined on the natural numbers as iterating the map \(C(x) = x/2\) when \(x \in \mathbb{N}\) is even and \(C(x) = 3x + 1\) when \(x\) is odd. Because \(3x + 1\) is always even when \(x\) is odd, it is also natural to consider a slight variant of \(C\), the map \(T\) where \(T(x) = x/2\) when \(x\) is even and \(T(x) = (3x + 1)/2\) when \(x\) is odd.

As of 2025, the conjecture had been computer-verified up to \(2^{71}\) [Barina, 2025].

The conjecture can be divided in two seemingly independent conjectures: (No divergent orbits conjecture) there are no \(x \in \mathbb{N}\) such that \(\lim_{n\to\infty} T^n(x) = +\infty\) and (No nontrivial cycles conjecture) the only cycle of \(T\) in \(\mathbb{N}^+\) is \(\{1, 2\}\). The latter is sometimes referred to as the "Weak Collatz conjecture" [Tao, 2011].

The Collatz problem beyond natural numbers

Although \(T\) and \(C\) are defined in \(\mathbb{N}\), there are no obstacles to looking at the Collatz map in the negative numbers. Three new cycles show up in the negative numbers: the cycle of \(-1\), the cycle of \(-5\) and the cycle of \(-17\) [Böhm and Sontacchi, 1978]. Furthermore, any negative number seems to reach one of these cycles.

It turns out that Collatz iterations are more generally well-defined on all rational numbers with odd denominator¹ [Lagarias, 1985]: the parity of such a rational is defined as the parity of its numerator, dividing by 2 and computing \(3x + 1\) preserve odd denominators.

A natural generalisation of the no-divergent-orbits part of the Collatz conjecture to the rationals is:

The Collatz problem is hard

The Collatz problem is notoriously extremely hard and its solution seems to be still very far away in spite of more than half a century of research, wonderfully summarised in Jeffrey C. Lagarias's annotated bibliographies [Lagarias, 2003][Lagarias, 2006] and overview [Lagarias, 2021].

Famously, mathematician Paul Erdős said that "Mathematics is not yet ready for such problems" and, reportedly, he would also have described the problem as "Hopeless. Absolutely hopeless". As a warning, the Collatz problem is also given as Problem 2 in Richard Guy's 1983 paper "Don't try to solve these problems!" [Guy, 1983].

Proof Assistants

Proof assistants are software tools able to express and verify formal proofs. Popular proof assistants include Lean, Coq/Rocq, Isabelle, HOL Light and Metamath. Using a proof assistant to formalise a result immensely facilitates scientific consensus on its correctness: once a proof is verified by the tool, trust only relies on the (relatively small and well-audited) proof-checking kernel, not on the complexity of the proof itself.

Milestones in the use of proof assistants include the Coq proofs of the four-colour theorem [Gonthier, 2008] and the Feit-Thompson theorem on odd order finite groups [Gonthier et al., 2013], the HOL Light proof of the Kepler conjecture [Hales et al., 2017], and the liquid tensor experiment in Lean [Commelin et al., 2024].

References

• [Böhm and Sontacchi, 1978] Corrado Böhm and Giovanna Sontacchi. "On the existence of cycles of given length in integer sequences like \(x_{n+1} = x_n/2\) if \(x_n\) even, and \(x_{n+1} = 3x_n + 1\)". In: Atti della Accademia Nazionale dei Lincei. Rendiconti 64 (1978), pp. 260–264.
• [Barina, 2025] David Barina. "Improved verification limit for the convergence of the Collatz conjecture". In: The Journal of Supercomputing 81, 810 (2025). doi:10.1007/s11227-025-07337-0 — pcbarina.fit.vutbr.cz
• [Commelin et al., 2024] Johan Commelin, Adam Topaz et al. "Liquid tensor experiment". 2024. doi:10.1017/exp.2024.7
• [Coxeter, 1971] H. S. M. Coxeter. Cyclic sequences and frieze patterns: The Fourth Felix Behrend Memorial Lecture, Vinculum 8. 1971.
• [Guy, 1983] Richard K. Guy. "Don't Try to Solve These Problems!" In: The American Mathematical Monthly 90.1 (1983), pp. 35–41.
• [Gonthier, 2008] Georges Gonthier. "Formal proof — The four-color theorem". In: Notices of the American Mathematical Society 55.11 (2008), pp. 1382–1393.
• [Gonthier et al., 2013] Georges Gonthier et al. "A machine-checked proof of the odd order theorem". In: Interactive Theorem Proving (ITP 2013). Springer, 2013, pp. 163–179. doi:10.1007/978-3-642-39634-2_14
• [Hales et al., 2017] Thomas Hales et al. "A formal proof of the Kepler conjecture". In: Forum of Mathematics, Pi 5 (2017), e2. doi:10.1017/fmp.2017.1
• [Lagarias, 1985] Jeffrey C. Lagarias. "The \(3x + 1\) Problem and Its Generalizations". In: The American Mathematical Monthly 92.1 (1985), pp. 3–23.
• [Lagarias, 2003] Jeffrey C. Lagarias. The \(3x + 1\) problem: An annotated bibliography (1963–1999) (sorted by author). 2003. arXiv:math/0309224
• [Lagarias, 2006] Jeffrey C. Lagarias. The \(3x + 1\) Problem: An Annotated Bibliography, II (2000–2009). 2006. arXiv:math/0608208
• [Lagarias, 2021] Jeffrey C. Lagarias. "The 3x+1 Problem: An Overview". 2021. arXiv:2111.02635
• [Tao, 2011] Terence Tao. "The Collatz conjecture, Littlewood-Offord theory, and powers of 2 and 3". 2011. Blog post

Related Links

---

¹ Rationals with odd denominators exactly correspond to eventually-periodic 2-adic integers: Collatz iterations are more generally naturally defined on all 2-adic integers (\(\mathbb{Z}_2\)) [Lagarias, 1985].