Documentation

FormalConjectures.ErdosProblems.«686»

Erdős Problem 686 #

Reference: erdosproblems.com/686

theorem Erdos686.erdos_686 :
(∀ N2, k2, ∃ (n : ), mn + k, N = (∏ iFinset.Icc 1 k, (m + i)) / (∏ iFinset.Icc 1 k, (n + i))) sorry

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$?