Number theory

Erdős problem 930

Is it true that, for every

r

, there is a

k

such that if

I_1,\ldots,I_r

are disjoint intervals of consecutive integers, all of length at least

k

, then

\prod_{1\leq i\leq r}\prod_{m\in I_i}m

is not a perfect power?

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«930»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos930.erdos_930" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

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)

Original conjecture source: FormalConjectures/ErdosProblems/930.lean

Source type SHA-256: sha256:a3172ae86bfc8ac0c80d9332595d33db458db0dc4dd107b7b45a7ffc7ce461f4
Task id: fc-v2-erdos930-erdos-930-39abdc4cfd7ba51beb99f55a-formalized
Task commitment: sha256:c215a4cd6c86b5ffe72cf244c7525af7f87dcafb6d1389d4bf7c354b80610e35

References

erdosproblems.com/930

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

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)