Erdős Problem 930

Reference: erdosproblems.com/930

def Erdos930.IsPower (n : ℕ) : Prop

$n$ is a perfect power if there exist natural numbers $m$ and $l$ such that $1 < l$ and $m^l = n$.

Equations

• Erdos930.IsPower n = ∃ (m : ℕ) (l : ℕ), 1 < l ∧ m ^ l = n

theorem Erdos930.erdos_930 : sorry ↔ ∀ r > 0, ∃ (k : ℕ), ∀ (I₁ I₂ : Fin r → ℕ), (∀ (i : Fin r), 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) → (∀ (i j : Fin r), i < j → I₂ i < I₁ j) → ¬IsPower (∏ i : Fin r, ∏ m ∈ Finset.Icc (I₁ i) (I₂ i), m)

Is it true that, for every $r$, there is a $k$ such that if $I_1,\ldots,I_r$ are disjoint intervals of consecutive integers, all of length at least $k$, then $$ \prod_{1\leq i\leq r}\prod_{m\in I_i}m $$ is not a perfect power?

def Erdos930.nextPrime (k : ℕ) : ℕ

Returns the least prime satisfying $k \le p$

Equations

• Erdos930.nextPrime k = Nat.find ⋯

theorem Erdos930.erdos_930.variant.consecutive_strong (k l n : ℕ) : 3 ≤ k → 2 ≤ l → nextPrime k ≤ n + k → ∃ (p : ℕ), k ≤ p ∧ Nat.Prime p ∧ ¬l ∣ (∏ m ∈ Finset.Icc (n + 1) (n + k), m).factorization p

Let $k$, $l$, $n$ be integers such that $k \ge 3$, $l \ge 2$ and $n + k \ge p^{(k)}$, where $p^{(k)}$ is the least prime satisfying $p^{(k)} \ge k$. Then there is a prime $p \ge k$ for which $l$ does not divide the multiplicity of the prime factor $p$ in $(n + 1) \ldots (n + k)$.

Theorem 2 from [ErSe75].

[ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.

theorem Erdos930.erdos_930.variant.consecutive_integers (n k : ℕ) : 0 ≤ n → 2 ≤ k → ¬IsPower (∏ m ∈ Finset.Icc (n + 1) (n + k), m)

Erdos and Selfridge [ErSe75] proved that the product of consecutive integers is never a power (establishing the case $r=1$).

Theorem 1 from [ErSe75].

It is implied from erdos_930.variant.consecutive_strong.

[ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.