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
For and any , the sequence is not additively complete; equivalently is not a "good pair". A partial result on the open Erdős Problem 349: it complements complete_for_alpha_in_Ioo_one_to_goldenRatio.
The proof is recorded via the formal_proof mechanism rather than written inline, as it exceeds the repository's proof-length guideline.
∀ (t α : ℝ), 0 < t → 2 < α → ¬Erdos349.IsGoodPair t α