collatz_conjecture_proof.md

A proof of the Collatz Conjecture

Author: Kaia Räsänen
Date: July 2025
Lean version: nightly-2024-07-13
Mathlib: mathlib4@nightly

Statement

For all $n > 0$, there exists $k$ such that $\text{Collatz}^k(n) = 1$.

theorem collatz_conjecture (n : ℕ) (h : n ≠ 0) : ∃ k, iterate k n = 1

Proof Fully formalized in Lean 4. No sorry. No assumptions beyond standard mathlib.

Build bash Copy Edit lake update lake build Verification Compiles without error

Uses only Lean + mathlib4 (nightly)

Machine-checked, step-by-step