9.2. Source Entries🔗

Definition9.2.1

The Collatz step sends an even natural number n to n / 2 and an odd one to 3 * n + 1.

Lean code for Definition9.2.1

def collatzStep (n : Nat) : Nat :=
  if n % 2 == 0 then n / 2 else 3 * n + 1

def collatzTerminatesAtOne (n : Nat) : Prop :=
  ∃ steps : Nat, Nat.repeat collatzStep steps n = 1

Theorem9.2.2

groupuses 1used by 0⚠L∃∀N

EffortmediumTagsplayfulfamousincomplete

For every positive natural number n, repeated application of the Collatz step eventually reaches 1. This is the usual termination statement of the Collatz conjecture, phrased in terms of Definition 9.2.1.

Proof for Theorem 9.2.2

uses 0

No proof is currently known. This theorem is intentionally left unfinished so the generated graph and summary show an in-progress goal immediately.

Lean code for Theorem9.2.2

theorem declaration uses `sorry`collatz_conjecture (n : Nat) (hn : 0 < n) :
    collatzTerminatesAtOne n := byn:Nathn:0 < n⊢ collatzTerminatesAtOne n
  have hn' : 0 < n := hnn:Nathn:0 < nhn':0 < n⊢ collatzTerminatesAtOne n
  sorryAll goals completed! 🐙