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 αn≤1\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

The source's own material, retained exactly.

12 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

349.lean

Retained formal statement11 of 12

Erdős Problem 349, complete characterization on positive integer pairs. For integers t≥1t \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 t≥2t \ge 2 fails.

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