Erdős Problem 672

Reference: erdosproblems.com/672

def Erdos672With (k l : ℕ) [NeZero k] : Prop

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

Equations

• Erdos672With k l = ∀ (s : Fin k → ℕ), 0 < s 0 → (∃ d > 0, (s 0).gcd d = 1 ∧ ∀ (i : Fin k), s i = s 0 + ↑i * d) → ¬∃ (q : ℕ), ∏ i : Fin k, s i = q ^ l

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

Can the product of an arithmetic progression of positive integers of length ≥ 4 be a perfect power?

theorem erdos_672.variants.euler : Erdos672With 4 2

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

theorem 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.