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
Binary expansion. Every natural number is a sum of distinct powers of two: there is a finite set of exponents with . Proved by strong induction: subtract the largest power , recurse on the remainder.
∀ (k : ℕ), ∃ E, k = ∑ i ∈ E, 2 ^ i