Artifact · conjectured
Collatz conjecture
This page records one proposition and the evidence attached to it. Text from the source ledger is shown as record data.
- Identifier
- F:collatz-reaches-one
- Proof route
- Not assigned
- External status
- open
- Axiom footprint
- Empty
Recorded description
Iterating the map that halves an even number and sends an odd number m to 3m+1 reaches 1 from every positive starting value.
theorem Collatz.reaches_one : forall (n : Nat), 0 < n -> exists k : Nat, (fun m => if m % 2 = 0 then m / 2 else 3 * m + 1)^[k] n = 1Dependencies
The graph shows direct ledger edges. Follow a node to open its artifact page.
0 direct dependencies 0 direct dependents
Evidence
Provenance
{
"date": "2026-08-14",
"established_by": "not established in this ledger",
"source": "proposition extracted from the S:number strand of the math-education concept graph; statement authored here, nothing copied",
"prior_art": [
{
"citation": "Collatz, circa 1937",
"establishes": "the conjecture; still open"
}
]
}