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 statement5 of 8

Can 99 be written as 9=∏1≤i≤k(m+i)∏1≤i≤k(n+i)9=\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_686.variants.nine1 lineExact file
True ↔ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 9 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))
SolvedStatement only, no proof