Erdős Problem #1211
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`IsNatPartition A B` says that `A` and `B` are disjoint and `A ∪ B` is all of `ℕ`. Here `ℕ` contains \(0\). This is harmless: \(0\) adds nothing to a sum of distinct elements and does not count in the density below, so partitions of `ℕ` and of the positive integers give the same values.
The upper logarithmic density \[\overline{\delta}(X)=\limsup_{x\to\infty}\frac{1}{\log x}\sum_{n\in X,\ n<x}\frac{1}{n}\] of a set `X` of natural numbers, with a real cutoff `x`. The sum runs over the positive integers `n < x` in `X`, written as `1 ≤ n < ⌈x⌉₊` (see `mem_Ico_ceil_iff`). The quotient is eventually at most \(1 + 1/\log x\), so the `limsup` is not a junk value.
The larger of the upper logarithmic densities of the subset-sum sets of the two classes, \(\max(\overline{\delta}(S(A)),\overline{\delta}(S(B)))\). Here `subsetSums A` is the set of sums of finitely many distinct elements of `A`; it contains the empty sum \(0\), which does not affect the density.
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.