/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 930
open Finset
namespace Erdos930
$n$ is a perfect power if there exist natural numbers $m$ and $l$ such that $1 < l$ and $m^l = n$.
def IsPower (n : ℕ) : Prop :=
∃ m l, 1 < l ∧ m^l = n
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?
@[category research open, AMS 11]
theorem erdos_930 :
answer(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 ∈ Icc (I₁ i) (I₂ i), m) := ⊢ True ↔
∀ 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, ∏ m ∈ Icc (I₁ i) (I₂ i), m)
All goals completed! 🐙
Returns the least prime satisfying $k \le p$
def nextPrime (k : ℕ) : ℕ :=
Nat.find (Nat.exists_infinite_primes k)
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.
@[category research solved, AMS 11]
theorem erdos_930.variants.consecutive_strong :
∀ k l n, 3 ≤ k → 2 ≤ l → nextPrime k ≤ n + k →
∃ p, k ≤ p ∧ p.Prime ∧
¬ (l ∣ Nat.factorization (∏ m ∈ Icc (n + 1) (n + k), m) p) := ⊢ ∀ (k l n : ℕ),
3 ≤ k → 2 ≤ l → nextPrime k ≤ n + k → ∃ p, k ≤ p ∧ Nat.Prime p ∧ ¬l ∣ (∏ m ∈ Icc (n + 1) (n + k), m).factorization p
All goals completed! 🐙
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.variants.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.
@[category research solved, AMS 11]
theorem erdos_930.variants.consecutive_integers :
∀ n k, 0 ≤ n → 2 ≤ k →
¬ IsPower (∏ m ∈ Icc (n + 1) (n + k), m) := ⊢ ∀ (n k : ℕ), 0 ≤ n → 2 ≤ k → ¬IsPower (∏ m ∈ Icc (n + 1) (n + k), m)
All goals completed! 🐙
end Erdos930