Erdős Problem 672

Reference: erdosproblems.com/672

def Erdos672.Erdos672With (k l : ℕ) : Prop

Erdős problem 672 conjectures that the below holds for any $k ≥ 4$ and $l > 1$.

Equations

• Erdos672.Erdos672With k l = ∀ (s : Finset ℕ), s.card = k → ∃ n > 0, ∃ d > 0, n.gcd d = 1 → (↑s).IsAPOfLengthWith (↑k) n d → ∀ (q : ℕ), ∏ i ∈ s, i ≠ q ^ l

theorem Erdos672.erdos_672 : (∀ (k l : ℕ), l > 1 → k ≥ 4 → Erdos672With k l) ↔ sorry

Can the product of an arithmetic progression of positive integers $n, n + d, ..., n + (k - 1)d$ of length ≥ 4, with $(n, d) = 1$, be a perfect power?

theorem Erdos672.erdos_672.variants.euler : Erdos672With 4 2

According to https://www.erdosproblems.com/672, Euler proved this.

theorem Erdos672.erdos_672.variants.oblath : Erdos672With 5 2 ∧ Erdos672With 3 3 ∧ Erdos672With 3 4 ∧ Erdos672With 3 5

According to https://www.erdosproblems.com/672, Obláth proved this.

[Ob51] Oblath, Richard, Eine Bemerkung über Produkte aufeinander folgender Zahlen. J. Indian Math. Soc. (N.S.) (1951), 135-139.