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 any there exists some such that the set of such that the sequence is complete consists of at least disjoint line segments.
∀ (k : ℕ), ∃ t ∈ Set.Ioo 0 1, ∃ ι, ↑k ≤ Set.univ.encard ∧ ∃ I, (∀ (i : ι), 2 ≤ (I i).encard ∧ (I i).Nonempty ∧ IsConnected (I i)) ∧ Pairwise (Function.onFun Disjoint I) ∧ ⋃ i, I i ⊆ {α | α > 0 ∧ Erdos349.IsGoodPair t α}SolvedStatement only, no proof