Erdős problem 330 · problems.science

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?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

330.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/330.leanErdos330.erdos_330_statement4 linesExact file

1True ↔2  ∃ A h,3    Erdos330.MinAsymptoticAddBasisOfOrder A h ∧4      0 < A.upperDensity ∧ ∀ n ∈ A, 0 < (Erdos330.UnrepWithout A n h).upperDensity

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.

Sources

Search problems.science