3.1. Side-by-Side Views
These grafts reuse the Collatz entries below. A full card keeps the explanatory definition together with its attached Lean code, while compact cards keep the statement and proof facets easy to compare.
-
collatzStep[complete] -
collatzTerminatesAtOne[complete]
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 DefinitionStep
Associated Lean declarations
-
collatzStep[complete]
-
collatzTerminatesAtOne[complete]
-
collatzStep[complete] -
collatzTerminatesAtOne[complete]
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
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.
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.
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.