Erdős Problem 137

References:

• erdosproblems.com/137

theorem Erdos137.erdos_137 : (∀ k ≥ 3, ∀ (n : ℕ), ¬(∏ x ∈ Finset.Ioc n (n + k), x).Powerful) ↔ sorry

Let $k\geq 3$. Can the product of any $k$ consecutive integers $N$ ever be powerful? That is, must there always exist a prime $p\mid N$ such that $p^2\nmid N$?

theorem Erdos137.erdos_137.variants.perfect_power (k : ℕ) (hk : k ≥ 2) (n x l : ℕ) (hl : 2 ≤ l) : ∏ x ∈ Finset.Ioc n (n + k), x ≠ x ^ l

Let $k\geq 2$. Erdős and Selfridge [ES75] proved that the product of any $k$ consecutive integers $N$ cannot be a perfect power.

[ES75] P. Erdös, J. L. Selfridge, "The product of consecutive integers is never a power", Illinois J. Math. 19(2): 292-301, 1975

theorem Erdos137.erdos_137.multiple_powerful_factors (m k : ℕ) (hm : 0 < m) : ∃ (n₀ : ℕ), ∀ n > n₀, ∃ (P : Finset ℕ), P.card = k ∧ ∀ p ∈ P, Nat.Prime p ∧ p ∣ ∏ x ∈ Finset.Ioc m (m + n), x ∧ ¬p ^ 2 ∣ ∏ x ∈ Finset.Ioc m (m + n), x

Erdős [Er82c] conjectures that, if $m$, $k$ are fixed and $n$ sufficiently large, then there must be at least $k$ distict primes $p$ such that $p\mid m(m+1)\cdots (m+n)$ and yet $p^2$ does not divide the right hand side.

[Er82c] Erdős, Paul, "Miscellaneous problems in number theory". Congr. Numer. (1982), 25-45.,