Is it true that, for every $r$ , there is a $k$ such that if $I_{1}, \dots, I_{r}$ are disjoint intervals of consecutive integers, all of length at least $k$ , then $1 \leq i \leq r \prod m \in I_{i} \prod m$ is not a perfect power?

unreviewedOpen. Best to date: partial proof, not yet machine-sealed.

number theory · open · formalized (Lean) · 2 attempts

Check This Result Yourself

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence2

partial proof

unverified claim

#930 (multi-block Erdős–Selfridge) is OPEN and NOT settled by the known Erdős–Graham counterexamples, which fix block length and grow the number of blocks r — the DUAL quantifier order of #930 (which

partial proof

unverified claim

Erdos #930 OPEN (r>=2). Reframed r-block square as squarefree-part/parity identity (perfect-power analog of #931 radical equality); RIGOROUS NEGATIVE TRANSFER: Stormer/S-unit/bounded-cofactor from #93

Transfer from #931: the incidence/MATCHING VIEW (large primes p>=k divide one term per block, odd-multiplicity primes must be parity-matched across blocks) transfers and gives the right reframing; the Stormer FINITENESS ENGINE does NOT transfer because #930 imposes no smoothness constraint (any primes allowed, only multiplicities ==0 mod l). r=1 = Erdos-Selfridge. No solve, no new finiteness theorem, no counterexample. Verified by sympy exact factorization; r=2 k>=5 emptiness via squarefree-part hashing to a<4e5.

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Assuming the intervals are intervals of **positive** integers [[nomath]](if an interval is allowed to contain $0$, the product is $0$, which *is* a perfect power)[[/nomath]], then **this is currently an open problem**. It appears as **Erdős Problem #930**. ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

Formal proof

AMS 11 · open (literature)

theorem erdos_930 :
    answer(sorry) ↔ ∀ 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) →
          ¬ IsPower (∏ i : Fin r, ∏ m ∈ Icc (I₁ i) (I₂ i), m)

formal-conjectures/930.lean ↗

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela