Skip to content

Erdős problem 930

Start work

Is it true that, for every rr, there is a kk such that if I1,…,IrI_1,\ldots,I_r are disjoint intervals of consecutive integers, all of length at least kk, then ∏1≤i≤r∏m∈Iim \prod_{1\leq i\leq r}\prod_{m\in I_i}m is not a perfect power?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

930.lean

Retained formal statement1 of 3

Is it true that, for every rr, there is a kk such that if I1,…,IrI_1,\ldots,I_r are disjoint intervals of consecutive integers, all of length at least kk, then ∏1≤i≤r∏m∈Iim \prod_{1\leq i\leq r}\prod_{m\in I_i}m is not a perfect power?

FormalConjectures/ErdosProblems/930.leanErdos930.erdos_9306 linesExact file
True ↔  ∀ r > 0,    ∃ k,      ∀ (I₁ I₂ : Fin r → ℕ),        (∀ (i : Fin r), 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) →          (∀ (i j : Fin r), i < j → I₂ i < I₁ j) → ¬Erdos930.IsPower (∏ i, ∏ m ∈ Finset.Icc (I₁ i) (I₂ i), m)
OpenStatement only, no proof