collatz_generalization_5x1
Disprovedconjecturediscrete-mathematicsdynamical-systemsnumber-theory
5x+1 problem (open analogue of Collatz): Starting from any positive integer, if even halve it, if odd apply (5x+1)/2. Does every sequence reach 1? Unlike 3x+1 where all checked, the 5x+1 iteration may diverge. Open; believed to have diverging sequences.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem collatz_generalization_5x1 :
∀ n : ℕ, 1 ≤ n →
∃ k : ℕ, (Nat.rec n (fun _ m =>
if m % 2 = 0 then m / 2 else (5 * m + 1) / 2) k = 1) := by
sorrySource