Erdős Problem 686

Reference: erdosproblems.com/686

theorem Erdos686.erdos_686 : True ↔ ∀ N ≥ 2, ∃ k ≥ 2, ∃ (n : ℕ), ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

Can every integer $N≥2$ be written as $$N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

theorem Erdos686.erdos_686.variants.square : True ↔ ∀ N ≥ 2, IsSquare N → ∃ k ≥ 2, ∃ (n : ℕ), ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

Can every square $N≥2$ be written as $$N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

theorem Erdos686.erdos_686.variants.four : True ↔ ∃ k ≥ 2, ∃ (n : ℕ), ∃ m ≥ n + k, 4 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

Can $4$ be written as $$4=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

theorem Erdos686.erdos_686.variants.four_two : ¬∃ (n : ℕ), ∃ m ≥ n + 2, 4 = ↑(∏ i ∈ Finset.Icc 1 2, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 2, (n + i))

The number $4$ cannot be written as $$4=\frac{\prod_{1\leq i\leq 2}(m+i)}{\prod_{1\leq i\leq 2}(n+i)}$$ for $m≥n+2$!

theorem Erdos686.erdos_686.variants.four_three : ¬∃ (n : ℕ), ∃ m ≥ n + 3, 4 = ↑(∏ i ∈ Finset.Icc 1 3, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 3, (n + i))

The number $4$ cannot be written as $$4=\frac{\prod_{1\leq i\leq 2}(m+i)}{\prod_{1\leq i\leq 2}(n+i)}$$ for $m≥n+2$!

See comment section on erdosproblems.com

theorem Erdos686.erdos_686.variants.nine : True ↔ ∃ k ≥ 2, ∃ (n : ℕ), ∃ m ≥ n + k, 9 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

Can $9$ be written as $$9=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

theorem Erdos686.erdos_686.variants.twenty_five : True ↔ ∃ k ≥ 2, ∃ (n : ℕ), ∃ m ≥ n + k, 25 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

Can $25$ be written as $$25=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?

theorem Erdos686.erdos_686.variants.non_square : True ↔ ∀ N ≥ 2, ¬IsSquare N → ∃ k ≥ 2, ∃ (n : ℕ), ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

Can every non-square $N≥2$ be written as $$N=\frac{\prod_{1\leq i\leq k}(m+i)}{\prod_{1\leq i\leq k}(n+i)}$$ for some $k≥2$ and $m≥n+k$?