Number theory

Erdős 686 - four

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

References

erdosproblems.com/686

[Er79d] Erdős, P., *Some unconventional problems in number theory*. Acta Math. Acad. Sci. Hungar. (1979), 71-80.

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 4 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

What you must prove

import FormalConjectures.ErdosProblems.«686»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos686.erdos_686.variants.four" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/686.lean

Source type SHA-256: sha256:ba400ba0844a1182de84df5aa217255c4343091b3aec968e35793bb0e75e8db2
Task id: fc-379fc029-variants-four-27f59536d7-formalized-v1
Task commitment: sha256:bd2f52489d971db4ae4a8c79e106c7fd3080827a8d4dc72f3154e395da098528

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.