Skip to content

Erdős problem 349

For 0<α10 < \alpha \le 1 and any t>0t > 0, (t,α)(t, \alpha) is not a good pair: every term tαn\lfloor t\alpha^n\rfloor lies in the finite interval [0,t][0, \lfloor t\rfloor] (since αn1\alpha^n \le 1), so every subset sum is bounded by the constant i[0,t]i\sum_{i \in [0,\lfloor t\rfloor]} i, and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, complementing the 2<α2 < \alpha and integer-coefficient cases.

Sources

Browse retained paths and inspect the exact material available for this Problem.

12 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

349.lean

Retained formal statement4 of 12

**The dyadic fiber at α=2\alpha = 2.** For every kk, the pair (1/2k,2)(1/2^k, 2) is good: the sequence 2n/2k\lfloor 2^n / 2^k\rfloor is additively complete because at index n=m+kn = m + k it equals the exact power 2m2^m, so its range contains all powers of two, which already form an additively complete set. Uses monotonicity IsAddComplete.mono.

FormalConjectures/ErdosProblems/349.leanErdos349.dyadic_two_isGoodPair1 lineExact file
∀ (k : ℕ), Erdos349.IsGoodPair (1 / 2 ^ k) 2
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page