Erdős problem 38
Does there exist which is not an additive basis, but is such that for every set of Schnirelmann density and every there exists such that where for ?
Sources
FormalConjectures/ErdosProblems/
38.lean
Does there exist which is not an additive basis, but is such that for every set of Schnirelmann density and every there exists such that where for ?
Note: here Erdős seems to use a slightly weaker notion of an additive basis (see [Er56] at the top of page 135). In particular, for this problem, a set is an additive basis of order if every natural number can be written as a sum of _at most_ elements of the set, rather than as a sum of _precisely_ elements.
A positive [solution](https://github.com/spicylemonade/erdos-38) was given by GPT 5.5 Pro (prompted by gebyjaff, cleanup by Liam Price); in fact a sparse random set has this property, with .
True ↔ ∃ B, ¬B.IsWeakAddBasis ∧ ∃ f, (∀ (α : ℝ), 0 < α → α < 1 → f α > 0) ∧ ∀ (A : Set ℕ) (N : ℕ), have α := schnirelmannDensity A; ∃ b ∈ B, ↑(Set.Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * ↑N