Skip to content

Erdős problem 741

Start work

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

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

741.lean

Retained formal statement1 of 4

Let A⊆NA\subseteq \mathbb{N} be such that A+AA+A has positive upper density. 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 upper density?

This was proved by the DeepMind prover agent.

FormalConjectures/ErdosProblems/741.leanErdos741.erdos_741.parts.i4 linesExact file
True ↔  ∀ (A : Set ℕ),    0 < (A + A).upperDensity →      ∃ 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.