erdős #930
Is it true that, for every , there is a such that if are disjoint intervals of consecutive integers, all of length at least , thenis not a perfect power?
Open — best to date is a partial proof, not yet sealed.
number theory · open · formalized (Lean) · 2 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
partial proof
needs verification
#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
needs verification
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
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 ↗status
open