3.2. Source Entries🔗

Definition3.2.1

group

Statement uses 2

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

The Collatz step sends an even natural number n to n / 2 and an odd one to 3 * n + 1. The odd branch combines Definition 2.1 with Definition 1.1.

Lean code for Definition3.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

Theorem3.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 3.2.1.

Proof for Theorem 3.2.2

uses 0

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

Lean code for Theorem3.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! 🐙