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 statement1 of 4

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive upper density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive upper density?

This was proved by the DeepMind prover agent.

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

1True ↔2  ∀ (A : Set ℕ),3    0 < (A + A).upperDensity →4      ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

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