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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/930.lean

Formal Conjectures

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

Continue

Start a contributionBrowse the source filesOpen the collection entry