Erdős Problem 936

Reference: erdosproblems.com/936

def EventuallyNotPowerful (a : ℕ → ℕ) : Prop

The predicate that a n is only powerful for finitely many n.

Equations

• EventuallyNotPowerful a = ∀ᶠ (n : ℕ) in Filter.atTop, ¬(a n).Powerful

theorem erdos_936.variants.two_pow_add_one : (EventuallyNotPowerful fun (x : ℕ) => 2 ^ x + 1) ↔ sorry

Is $2^n + 1$ powerful for finitely many $n$?

theorem erdos_936.variants.two_pow_sub_one : (EventuallyNotPowerful fun (x : ℕ) => 2 ^ x - 1) ↔ sorry

Is $2^n - 1$ powerful for finitely many $n$?

theorem erdos_936.variants.factorial_add_one : (EventuallyNotPowerful fun (x : ℕ) => x.factorial + 1) ↔ sorry

Is $n! + 1$ powerful for finitely many $n$?

theorem erdos_936.variants.factorial_sub_one : (EventuallyNotPowerful fun (x : ℕ) => x.factorial - 1) ↔ sorry

Is $n! - 1$ powerful for finitely many $n$?