Erdős problem 741 · problems.science

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive density in the literal sense that its natural density exists and is positive. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density in this sense?

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

741.lean

Retained formal statement2 of 4

Is there a basis $A$ of order $2$ such that if $A=A_1\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?

This was proved by DeepMind prover agent.

FormalConjectures/ErdosProblems/741.leanErdos741.erdos_741.parts.ii4 linesExact file

1True ↔2  ∃ A,3    (A ∪ {0}).IsAddBasisOfOrder 2 ∧4      ∀ (A₁ A₂ : Set ℕ), A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬(IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂))

SolvedProof has a holeformal conjecturesexternal 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