Sign in Register

Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Collatz reachability

CollatzReachesdef

CollatzReaches m n holds when iterating collatzStep from m eventually gives n.

def CollatzReaches (m n : ℕ) : Prop :=
  Relation.ReflTransGen (fun a b => b = collatzStep a) m n

Builds on

Collatz step

Used by

Collatz conjecture

From Mathlib

Logic.Relation

import Conjectura.Defs.Mathematics.NumberTheory.CollatzReaches · maintainer — open · raw source

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