Erdős Problem #330

PROVED LEANdatabase updated 2026-05-11

The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

`Rep A m h` means `m` is a sum of exactly `h` elements of `A`, which is `m ∈ h • A`. Exactly `h` rather than at most `h`, for two reasons. It is the notion Erdős states the problem with, via `f_2(m)`, the number of solutions of `m = a_i + a_j` [Er80]. And it is the notion `IsAsymptoticAddBasisOfOrder` uses below, so the statement is not switching between two meanings of "representable" partway through. Allowing fewer than `h` summands also breaks the statement outright: taking one summand makes

Integers **not** representable as a sum of exactly `h` elements of `A` **while avoiding** `n`.

An asymptotic additive basis of order `h` is minimal when one cannot obtain an asymptotic additive basis by removing any element from it.

Does there exist a minimal basis \(A \subset \mathbb{N}\) with positive density such that, for any \(n \in A\), the (upper) density of integers which cannot be represented without using \(n\) is positive? Neither set is asked to have a density, only to have positive upper density, so `Set.upperDensity` is used for both rather than `Set.HasPosDensity`. As with many of Erdős' questions "positive density" here most likely means positive upper density, and in [Er80] he considers either the lower or the upper density for the integers not representable without a fixed `n`. Requiring the density to exist would ask a strictly harder question than the one posed. See #3979. Such a set exists, so the answer is yes. The linked proof gives one of order `2`.

Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/330.

Prizenone

Topicsnumber theory, additive basis

Statement in LeanFormal Conjectures

Solution in Leanyes

Original pageerdosproblems.com/330

Attempts

submit one →

NOBODY HAS SENT US AN ATTEMPT YET

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.

← #329 the board #331 →