Collatz conjecture

Open

CollatzConjecture.collatz_conjecture

by mysticflounder · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

Retired because this duplicated the existing theorem collatz_conjecture. Use the existing theorem collatz_conjecture instead.

Preamble

import Definitions.Def_collatzStep

Formal statement

namespace CollatzConjecture
theorem collatz_conjecture (n : ℕ) (hn : n > 0) : ∃ m, collatzStep^[m] n = 1 := by sorry
end CollatzConjecture

Source

google-deepmind/formal-conjectures, FormalConjectures/Wikipedia/CollatzConjecture.lean, theorem collatz_conjecture (lines 368-381): https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/CollatzConjecture.lean; mathematical reference: https://en.wikipedia.org/wiki/Collatz_conjecture

View graph