Erdős Problem 364

Reference: erdosproblems.com/364

theorem Erdos364.erdos_364 : ¬∃ (n : ℕ), n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful

There is no consecutive triple of powerful numbers.

theorem Erdos364.erdos_364.variants.strong : ∃ (c : ℝ) (_ : c > 0), ∀ (k : ℕ), ↑(Nat.nth Nat.Powerful (k + 2)) - ↑(Nat.nth Nat.Powerful k) > ↑(Nat.nth Nat.Powerful k) ^ c

Erdős [Er76d] conjectured a stronger statement: if $n_k$ is the $k$th powerful number, then $n_{k+2} - n_k > n_k^c$ for some constant $c > 0$.

[Er76d] Erdős, P., Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44.

theorem Erdos364.erdos_364.variants.weak : ¬∃ (n : ℕ), n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerful

There is no quadruple of powerful numbers, since at least one of the four numbers must be $2 \pmod{4}$, which cannot be powerful (since $2$ divides it, but $2^2$ does not).