Collatz conjecture

Conjectura.Statements.Mathematics.NumberTheory.CollatzConjecture

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Defs.Mathematics.NumberTheory.CollatzReaches

/-! # Collatz conjecture -/

namespace Conjectura.NumberTheory

/-- The **Collatz conjecture**: every positive integer `CollatzReaches` one. -/
def CollatzConjectureProp : Prop := ∀ n : ℕ, 0 < n → CollatzReaches n 1

end Conjectura.NumberTheory