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 statement11 of 12

Erdős Problem 349, complete characterization on positive integer pairs. For integers t1t \ge 1, α1\alpha \ge 1, the pair (t,α)(t, \alpha) is good (i.e. tαn\lfloor t\alpha^n\rfloor is additively complete) iff (t,α)=(1,2)(t, \alpha) = (1, 2). Assembles the four partial results: (1,2)(1,2) is good, α1\alpha \le 1 fails, 2<α2 < \alpha fails (alpha_gt_two_not_isGoodPair), and integer t2t \ge 2 fails.

FormalConjectures/ErdosProblems/349.leanErdos349.integer_isGoodPair_iff1 lineExact file
∀ (t α : ℤ), 1 ≤ t → 1 ≤ α → (Erdos349.IsGoodPairt ↑α ↔ t = 1 ∧ α = 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