Skip to content

Erdős problem 686

Start work

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

Sources

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

686.lean

Retained formal statement1 of 8

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

FormalConjectures/ErdosProblems/686.leanErdos686.erdos_6861 lineExact file
sorry ↔ ∀ N ≥ 2, ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
OpenStatement only, no proof