Skip to content

Erdős problem 741

Let A⊆NA\subseteq \mathbb{N} be such that A+AA+A has positive density in the literal sense that its natural density exists and is positive. Can one always decompose A=A1⊔A2A=A_1\sqcup A_2 such that A1+A1A_1+A_1 and A2+A2A_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 statement3 of 4

Let A⊆NA\subseteq \mathbb{N} be such that A+AA+A has positive density in the literal sense that its natural density exists and is positive. Can one always decompose A=A1⊔A2A=A_1\sqcup A_2 such that A1+A1A_1+A_1 and A2+A2A_2+A_2 both have positive density in this sense?

This was disproved by the DeepMind prover agent.

FormalConjectures/ErdosProblems/741.leanErdos741.erdos_741.variants.exact_density3 linesExact file
False ↔  ∀ (A : Set ℕ),    (A + A).HasPosDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ (A₁ + A₁).HasPosDensity ∧ (A₂ + A₂).HasPosDensity
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.

Search problems.science

Find a Problem, Result, source, or page