Skip to content

Erdős problem 38

Does there exist BNB \subset \mathbb{N} which is not an additive basis, but is such that for every set ANA \subseteq \mathbb{N} of Schnirelmann density α\alpha and every NN there exists bBb \in B such that (A(A+b)){1,,N}(α+f(α))N \lvert (A \cup (A+b)) \cap \{1, \ldots, N\} \rvert \geq (\alpha + f(\alpha)) N where f(α)>0f(\alpha) > 0 for 0<α<10 < \alpha < 1?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

38.lean

Retained formal statement1 of 1

Does there exist BNB \subset \mathbb{N} which is not an additive basis, but is such that for every set ANA \subseteq \mathbb{N} of Schnirelmann density α\alpha and every NN there exists bBb \in B such that (A(A+b)){1,,N}(α+f(α))N \lvert (A \cup (A+b)) \cap \{1, \ldots, N\} \rvert \geq (\alpha + f(\alpha)) N where f(α)>0f(\alpha) > 0 for 0<α<10 < \alpha < 1?

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 kk if every natural number can be written as a sum of _at most_ kk elements of the set, rather than as a sum of _precisely_ kk 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 BB has this property, with f(α)α(1α)2f(\alpha)\gg \alpha (1-\alpha)^2.

FormalConjectures/ErdosProblems/38.leanErdos38.erdos_388 linesExact file
TrueB,    ¬B.IsWeakAddBasisf,        (∀ (α : ℝ), 0 < α → α < 1 → f α > 0) ∧          ∀ (A : Set ℕ) (N : ℕ),            have α := schnirelmannDensity A;bB, ↑(Set.Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * ↑N
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page