Erdős problem 349
For and any , is not a good pair: every term lies in the finite interval (since ), so every subset sum is bounded by the constant , and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, complementing the and integer-coefficient cases.
Sources
FormalConjectures/ErdosProblems/
349.lean
Retained formal statement
Erdős Problem 349, complete characterization on positive integer pairs. For integers , , the pair is good (i.e. is additively complete) iff . Assembles the four partial results: is good, fails, fails (alpha_gt_two_not_isGoodPair), and integer fails.
∀ (t α : ℤ), 1 ≤ t → 1 ≤ α → (Erdos349.IsGoodPair ↑t ↑α ↔ t = 1 ∧ α = 2)